chore(Topology): fix a typo (#10070)

There is no `NeBot` in this lemma
leanprover-community · Jan 28, 2024 · e975e78 · e975e78
1 parent 19b5ded
commit e975e78
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 11 deletions.
diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean
@@ -1329,9 +1329,12 @@ theorem mem_closure_iff_clusterPt : x ∈ closure s ↔ ClusterPt x (𝓟 s) :=
   mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm
 #align mem_closure_iff_cluster_pt mem_closure_iff_clusterPt
 
-theorem mem_closure_iff_nhds_neBot : x ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ :=
+theorem mem_closure_iff_nhds_ne_bot : x ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ :=
   mem_closure_iff_clusterPt.trans neBot_iff
-#align mem_closure_iff_nhds_ne_bot mem_closure_iff_nhds_neBot
+#align mem_closure_iff_nhds_ne_bot mem_closure_iff_nhds_ne_bot
+
+@[deprecated] -- 28 January 2024
+alias mem_closure_iff_nhds_neBot := mem_closure_iff_nhds_ne_bot
 
 theorem mem_closure_iff_nhdsWithin_neBot : x ∈ closure s ↔ NeBot (𝓝[s] x) :=
   mem_closure_iff_clusterPt
@@ -1471,14 +1474,8 @@ theorem Dense.open_subset_closure_inter (hs : Dense s) (ht : IsOpen t) :
 
 theorem mem_closure_of_mem_closure_union (h : x ∈ closure (s₁ ∪ s₂))
     (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ := by
-  rw [mem_closure_iff_nhds_neBot] at *
-  rwa [←
-    calc
-      𝓝 x ⊓ principal (s₁ ∪ s₂) = 𝓝 x ⊓ (principal s₁ ⊔ principal s₂) := by rw [sup_principal]
-      _ = 𝓝 x ⊓ principal s₁ ⊔ 𝓝 x ⊓ principal s₂ := inf_sup_left
-      _ = ⊥ ⊔ 𝓝 x ⊓ principal s₂ := by rw [inf_principal_eq_bot.mpr h₁]
-      _ = 𝓝 x ⊓ principal s₂ := bot_sup_eq
-      ]
+  rw [mem_closure_iff_nhds_ne_bot] at *
+  rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h
 #align mem_closure_of_mem_closure_union mem_closure_of_mem_closure_union
 
 /-- The intersection of an open dense set with a dense set is a dense set. -/

diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
@@ -1503,7 +1503,7 @@ theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
     refine' disjoint_of_disjoint_of_mem disjoint_compl_left _ hU
     rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
   tfae_have 2 → 3
-  · refine' fun H a s => ⟨fun hd has => mem_closure_iff_nhds_neBot.mp has _, H s a⟩
+  · refine' fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has _, H s a⟩
     exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot
   tfae_have 3 → 1
   · exact fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩