chore(SetTheory/Ordinal/Topology): generalize theorems to SuccOrder (#20491)

This takes care of some easy targets, though other theorems in this file should generalize as well.

Author: vihdzp

Mathlib/SetTheory/Ordinal/Topology.lean

@@ -50,25 +50,26 @@ theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬IsLimit a := by
       exact isOpen_Ioo
     · exact (ha ha').elim
 
+@[deprecated SuccOrder.nhdsGT (since := "2025-01-05")]
 protected theorem nhdsGT (a : Ordinal) : 𝓝[>] a = ⊥ := SuccOrder.nhdsGT
 
 @[deprecated (since := "2024-12-22")] alias nhds_right' := Ordinal.nhdsGT
 
--- todo: generalize to a `SuccOrder`
-theorem nhdsLT_eq_nhdsNE (a : Ordinal) : 𝓝[<] a = 𝓝[≠] a := by
-  rw [← nhdsLT_sup_nhdsGT, Ordinal.nhdsGT, sup_bot_eq]
+@[deprecated SuccOrder.nhdsLT_eq_nhdsNE (since := "2025-01-05")]
+theorem nhdsLT_eq_nhdsNE (a : Ordinal) : 𝓝[<] a = 𝓝[≠] a :=
+  SuccOrder.nhdsLT_eq_nhdsNE a
 
 @[deprecated (since := "2024-12-22")] alias nhds_left'_eq_nhds_ne := nhdsLT_eq_nhdsNE
 
--- todo: generalize to a `SuccOrder`
-theorem nhdsLE_eq_nhds (a : Ordinal) : 𝓝[≤] a = 𝓝 a := by
-  rw [← nhdsLE_sup_nhdsGT, SuccOrder.nhdsGT, sup_bot_eq]
+@[deprecated SuccOrder.nhdsLE_eq_nhds (since := "2025-01-05")]
+theorem nhdsLE_eq_nhds (a : Ordinal) : 𝓝[≤] a = 𝓝 a :=
+  SuccOrder.nhdsLE_eq_nhds a
 
 @[deprecated (since := "2024-12-22")] alias nhds_left_eq_nhds := nhdsLE_eq_nhds
 
--- todo: generalize to a `SuccOrder`
+@[deprecated SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (since := "2025-01-05")]
 theorem hasBasis_nhds_Ioc (h : a ≠ 0) : (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
-  nhdsLE_eq_nhds a ▸ nhdsLE_basis_of_exists_lt ⟨0, h.bot_lt⟩
+  SuccOrder.hasBasis_nhds_Ioc_of_exists_lt ⟨0, Ordinal.pos_iff_ne_zero.2 h⟩
 
 @[deprecated (since := "2024-12-22")] alias nhdsBasis_Ioc := hasBasis_nhds_Ioc
 
@@ -80,7 +81,7 @@ theorem nhds_eq_pure : 𝓝 a = pure a ↔ ¬IsLimit a :=
 theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsLimit o → ∃ a < o, Set.Ioo a o ⊆ s := by
   refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_
   by_cases ho' : IsLimit o
-  · simp only [(hasBasis_nhds_Ioc ho'.ne_zero).mem_iff, ho', true_implies]
+  · simp only [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt ⟨0, ho'.pos⟩).mem_iff, ho', true_implies]
     refine exists_congr fun a => and_congr_right fun ha => ?_
     simp only [← Set.Ioo_insert_right ha, Set.insert_subset_iff, ho, true_and]
   · simp [nhds_eq_pure.2 ho', ho, ho']
@@ -95,8 +96,8 @@ theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
         (∀ x hx, f x hx ∈ s) ∧ bsup.{u, u} o f = a,
       ∃ (ι : Type u), Nonempty ι ∧ ∃ f : ι → Ordinal, (∀ i, f i ∈ s) ∧ ⨆ i, f i = a] := by
   tfae_have 1 → 2 := by
-    simp only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter', nhdsLE_eq_nhds]
-    exact id
+    simpa only [mem_closure_iff_nhdsWithin_neBot, inter_comm s, nhdsWithin_inter',
+      SuccOrder.nhdsLE_eq_nhds] using id
   tfae_have 2 → 3
   | h => by
     rcases (s ∩ Iic a).eq_empty_or_nonempty with he | hne

Mathlib/Topology/Order/Basic.lean

@@ -489,6 +489,22 @@ theorem Dense.topology_eq_generateFrom [OrderTopology α] [DenselyOrdered α] {s
       let _ := generateFrom (Ioi '' s ∪ Iio '' s)
       exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1
 
+theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt [OrderTopology α] [PredOrder α] {a : α}
+    (ha : ∃ u, a < u) : (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
+  PredOrder.nhdsGE_eq_nhds a ▸ nhdsGE_basis_of_exists_gt ha
+
+theorem PredOrder.hasBasis_nhds_Ioc [OrderTopology α] [PredOrder α] [NoMaxOrder α] {a : α} :
+    (𝓝 a).HasBasis (a < ·) (Set.Ico a ·) :=
+  PredOrder.hasBasis_nhds_Ioc_of_exists_gt (exists_gt a)
+
+theorem SuccOrder.hasBasis_nhds_Ioc_of_exists_lt [OrderTopology α] [SuccOrder α] {a : α}
+    (ha : ∃ l, l < a) : (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
+  SuccOrder.nhdsLE_eq_nhds a ▸ nhdsLE_basis_of_exists_lt ha
+
+theorem SuccOrder.hasBasis_nhds_Ioc [OrderTopology α] [SuccOrder α] {a : α} [NoMinOrder α] :
+    (𝓝 a).HasBasis (· < a) (Set.Ioc · a) :=
+  SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (exists_lt a)
+
 variable (α)
 
 /-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then

Mathlib/Topology/Order/OrderClosed.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 -/
+import Mathlib.Topology.Order.LeftRight
 import Mathlib.Topology.Separation.Hausdorff
 
 /-!
@@ -274,6 +275,12 @@ protected theorem PredOrder.nhdsLT [PredOrder α] : 𝓝[<] a = ⊥ := by
 
 @[deprecated (since := "2024-12-21")] protected alias PredOrder.nhdsWithin_Iio := PredOrder.nhdsLT
 
+theorem PredOrder.nhdsGT_eq_nhdsNE [PredOrder α] (a : α) : 𝓝[>] a = 𝓝[≠] a := by
+  rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]
+
+theorem PredOrder.nhdsGE_eq_nhds [PredOrder α] (a : α) : 𝓝[≥] a = 𝓝 a := by
+  rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]
+
 theorem Ico_mem_nhdsLT_of_mem (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b :=
   mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Ico_self
 
@@ -556,6 +563,12 @@ protected theorem SuccOrder.nhdsGT [SuccOrder α] : 𝓝[>] a = ⊥ := PredOrder
 
 @[deprecated (since := "2024-12-22")] alias SuccOrder.nhdsWithin_Ioi := SuccOrder.nhdsGT
 
+theorem SuccOrder.nhdsLT_eq_nhdsNE [SuccOrder α] (a : α) : 𝓝[<] a = 𝓝[≠] a :=
+  PredOrder.nhdsGT_eq_nhdsNE (α := αᵒᵈ) a
+
+theorem SuccOrder.nhdsLE_eq_nhds [SuccOrder α] (a : α) : 𝓝[≤] a = 𝓝 a :=
+  PredOrder.nhdsGE_eq_nhds (α := αᵒᵈ) a
+
 theorem Ioc_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b :=
   mem_of_superset (Ioo_mem_nhdsGT_of_mem H) Ioo_subset_Ioc_self