feat: order topologies of successor orders (leanprover-community#32455)

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: vihdzp

Mathlib.lean

@@ -7481,6 +7481,7 @@ public import Mathlib.Topology.Order.ProjIcc
 public import Mathlib.Topology.Order.Real
 public import Mathlib.Topology.Order.Rolle
 public import Mathlib.Topology.Order.ScottTopology
+public import Mathlib.Topology.Order.SuccPred
 public import Mathlib.Topology.Order.T5
 public import Mathlib.Topology.Order.UpperLowerSetTopology
 public import Mathlib.Topology.Order.WithTop

Mathlib/Order/Cover.lean

@@ -388,20 +388,27 @@ section LinearOrder
 
 variable [LinearOrder α] {a b c : α}
 
+@[to_dual ge_of_gt]
+theorem WCovBy.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a :=
+  not_lt.1 fun hac => hab.2 hac hcb
+
+@[to_dual ge_of_gt]
+theorem CovBy.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a :=
+  hab.wcovBy.le_of_lt
+
 theorem CovBy.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b := by
   rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
 
 @[to_dual existing]
 theorem CovBy.Iio_eq (h : a ⋖ b) : Iio b = Iic a := by
   rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
 
-@[to_dual ge_of_gt]
-theorem WCovBy.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a :=
-  not_lt.1 fun hac => hab.2 hac hcb
+theorem CovBy.Ioo_eq_Ico (h : a ⋖ b) (c : α) : Ioo a c = Ico b c :=
+  subset_antisymm (fun _x hx ↦ ⟨h.ge_of_gt hx.1, hx.2⟩) <| Ico_subset_Ioo_left h.lt
 
-@[to_dual ge_of_gt]
-theorem CovBy.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a :=
-  hab.wcovBy.le_of_lt
+@[to_dual existing]
+theorem CovBy.Ioo_eq_Ioc (h : a ⋖ b) (c : α) : Ioo c b = Ioc c a :=
+  subset_antisymm (fun _x hx ↦ ⟨hx.1, h.le_of_lt hx.2⟩) <| Ioc_subset_Ioo_right h.lt
 
 @[to_dual unique_right]
 theorem CovBy.unique_left (ha : a ⋖ c) (hb : b ⋖ c) : a = b :=

Mathlib/SetTheory/Ordinal/Topology.lean

@@ -9,6 +9,7 @@ public import Mathlib.SetTheory.Ordinal.Enum
 public import Mathlib.Tactic.TFAE
 public import Mathlib.Topology.Order.IsNormal
 public import Mathlib.Topology.Order.Monotone
+public import Mathlib.Topology.Order.SuccPred
 
 /-!
 ### Topology of ordinals
@@ -41,34 +42,17 @@ variable {s : Set Ordinal.{u}} {a : Ordinal.{u}}
 instance : TopologicalSpace Ordinal.{u} := Preorder.topology Ordinal.{u}
 instance : OrderTopology Ordinal.{u} := ⟨rfl⟩
 
--- todo: generalize to other well-orders
-theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬ IsSuccLimit a := by
-  refine ⟨fun h ha => ?_, fun ha => ?_⟩
-  · obtain ⟨b, c, hbc, hbc'⟩ :=
-      (mem_nhds_iff_exists_Ioo_subset' ⟨0, ha.bot_lt⟩ ⟨_, lt_succ a⟩).1
-        (h.mem_nhds rfl)
-    have hba := ha.succ_lt hbc.1
-    exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)
-  · rcases zero_or_succ_or_isSuccLimit a with (rfl | ⟨b, rfl⟩ | ha')
-    · rw [← bot_eq_zero, ← Set.Iic_bot, ← Iio_succ]
-      exact isOpen_Iio
-    · rw [← Set.Icc_self, Icc_succ_left, ← Ioo_succ_right]
-      exact isOpen_Ioo
-    · exact (ha ha').elim
-
--- todo: generalize to a `SuccOrder`
+@[deprecated SuccOrder.isOpen_singleton_iff (since := "2026-01-20")]
+theorem isOpen_singleton_iff : IsOpen ({a} : Set Ordinal) ↔ ¬ IsSuccLimit a :=
+  SuccOrder.isOpen_singleton_iff
+
+@[deprecated SuccOrder.nhds_eq_pure (since := "2026-01-20")]
 theorem nhds_eq_pure : 𝓝 a = pure a ↔ ¬ IsSuccLimit a :=
-  (isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff
-
--- todo: generalize this lemma to a `SuccOrder`
-theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s := by
-  refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_
-  by_cases ho' : IsSuccLimit o
-  · simp only [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt ⟨0, ho'.bot_lt⟩).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']
+  SuccOrder.nhds_eq_pure
+
+@[deprecated SuccOrder.isOpen_iff (since := "2026-01-20")]
+theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s :=
+  SuccOrder.isOpen_iff
 
 open List Set in
 theorem mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal) :
@@ -154,16 +138,9 @@ theorem isClosed_iff_bsup :
     apply H (type_ne_zero_iff_nonempty.2 hι)
     exact fun i hi => hf _
 
--- todo: generalize to other well-orders
-theorem isSuccLimit_of_mem_frontier (ha : a ∈ frontier s) : IsSuccLimit a := by
-  simp only [frontier_eq_closure_inter_closure, Set.mem_inter_iff, mem_closure_iff] at ha
-  by_contra h
-  rw [← isOpen_singleton_iff] at h
-  rcases ha.1 _ h rfl with ⟨b, hb, hb'⟩
-  rcases ha.2 _ h rfl with ⟨c, hc, hc'⟩
-  rw [Set.mem_singleton_iff] at *
-  subst hb; subst hc
-  exact hc' hb'
+@[deprecated SuccOrder.isSuccLimit_of_mem_frontier (since := "2026-01-20")]
+theorem isSuccLimit_of_mem_frontier (ha : a ∈ frontier s) : IsSuccLimit a :=
+  SuccOrder.isSuccLimit_of_mem_frontier ha
 
 @[deprecated Order.isNormal_iff_strictMono_and_continuous (since := "2025-08-21")]
 theorem isNormal_iff_strictMono_and_continuous (f : Ordinal.{u} → Ordinal.{u}) :

Mathlib/Topology/Order/SuccPred.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2025 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux, Violeta Hernández Palacios
+-/
+module
+
+public import Mathlib.Topology.Order.Basic
+public import Mathlib.Order.SuccPred.Limit
+
+/-!
+# Order topologies of successor or predecessor orders
+
+This file proves miscellaneous results under the assumption of `OrderTopology` plus either of
+`SuccOrder` or `PredOrder`.
+-/
+
+@[expose] public section
+
+variable {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
+  {a : α} {s : Set α}
+
+open Order Topology
+
+namespace SuccOrder
+variable [SuccOrder α]
+
+theorem isOpen_singleton_of_not_isSuccPrelimit (ha : ¬ IsSuccPrelimit a) : IsOpen {a} := by
+  obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff_exists_covBy a |>.mp ha
+  by_cases ha' : IsMax a
+  · convert isOpen_Ioi (a := b) using 1
+    rw [hb.Ioi_eq]
+    grind [IsMax]
+  · convert isOpen_Ioo (a := b) (b := Order.succ a) using 1
+    simp [(covBy_succ_of_not_isMax ha').Ioo_eq_Ioc, hb.Ioc_eq]
+
+variable [NoMaxOrder α]
+
+theorem isOpen_singleton_iff : IsOpen {a} ↔ ¬ IsSuccLimit a := by
+  nontriviality α
+  refine ⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩
+  · obtain ⟨l, u, h₁, h₂⟩ := mem_nhds_iff_exists_Ioo_subset' (by simpa using ha.not_isMin)
+      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (Set.mem_singleton a))
+    refine ha.isSuccPrelimit l ?_
+    rw [← succ_eq_iff_covBy]
+    simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂
+    exact h₂ _ ⟨lt_succ l, h₁.1.succ_le.trans_lt h₁.2⟩
+  · obtain (ha | ha) := not_isSuccLimit_iff.mp ha
+    · convert isOpen_Iio (a := Order.succ a) using 1
+      simp [ha.Iic_eq]
+    · exact isOpen_singleton_of_not_isSuccPrelimit ha
+
+theorem nhds_eq_pure {a : α} : 𝓝 a = pure a ↔ ¬ IsSuccLimit a :=
+  (isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff
+
+theorem isOpen_iff {s : Set α} : IsOpen s ↔
+    ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s := by
+  refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_
+  by_cases ho' : IsSuccLimit o
+  · rw [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff]
+    grind
+  · simp [nhds_eq_pure.2 ho', ho, ho']
+
+theorem isSuccLimit_of_mem_frontier {a : α} {s : Set α} (ha : a ∈ frontier s) : IsSuccLimit a := by
+  rw [← isOpen_singleton_iff.not_left]
+  rw [frontier_eq_closure_inter_closure] at ha
+  grind [mem_closure_iff, Set.Nonempty]
+
+end SuccOrder
+
+-- TODO: use `to_dual`
+namespace PredOrder
+variable [PredOrder α]
+
+theorem isOpen_singleton_of_not_isPredPrelimit (ha : ¬ IsPredPrelimit a) : IsOpen {a} :=
+  SuccOrder.isOpen_singleton_of_not_isSuccPrelimit (α := αᵒᵈ) (isSuccPrelimit_toDual_iff.not.2 ha)
+
+variable [NoMinOrder α]
+
+theorem isOpen_singleton_iff : IsOpen {a} ↔ ¬ IsPredLimit a :=
+  (SuccOrder.isOpen_singleton_iff (α := αᵒᵈ)).trans isSuccLimit_toDual_iff.not
+
+theorem nhds_eq_pure {a : α} : 𝓝 a = pure a ↔ ¬ IsPredLimit a :=
+  (isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff
+
+theorem isOpen_iff {s : Set α} : IsOpen s ↔
+    ∀ o ∈ s, IsPredLimit o → ∃ a, o < a ∧ Set.Ioo o a ⊆ s := by
+  refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_
+  by_cases ho' : IsPredLimit o
+  · rw [(PredOrder.hasBasis_nhds_Ioc_of_exists_gt (not_isMax_iff.1 ho'.not_isMax)).mem_iff]
+    grind
+  · simp [nhds_eq_pure.2 ho', ho, ho']
+
+theorem isPredLimit_of_mem_frontier {a : α} {s : Set α} (ha : a ∈ frontier s) : IsPredLimit a := by
+  rw [← isSuccLimit_toDual_iff]
+  exact SuccOrder.isSuccLimit_of_mem_frontier (α := αᵒᵈ) ha
+
+end PredOrder