[Merged by Bors] - chore: deprecate Ordinal.IsAcc and Ordinal.IsClosedBelow

Mathlib/SetTheory/Ordinal/Topology.lean

@@ -170,55 +170,45 @@ open Set Filter Set.Notation
 
 /-- An ordinal is an accumulation point of a set of ordinals if it is positive and there
 are elements in the set arbitrarily close to the ordinal from below. -/
+@[deprecated AccPt (since := "2026-05-24")]
 def IsAcc (o : Ordinal) (S : Set Ordinal) : Prop :=
   AccPt o (𝓟 S)
 
 /-- A set of ordinals is closed below an ordinal if it contains all of
 its accumulation points below the ordinal. -/
+@[deprecated IsClosed (since := "2026-05-24")]
 def IsClosedBelow (S : Set Ordinal) (o : Ordinal) : Prop :=
   IsClosed (Iio o ↓∩ S)
 
+set_option linter.deprecated false in
+@[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
 theorem isAcc_iff (o : Ordinal) (S : Set Ordinal) : o.IsAcc S ↔
     o ≠ 0 ∧ ∀ p < o, (S ∩ Ioo p o).Nonempty := by
-  dsimp [IsAcc]
-  constructor
-  · rw [accPt_iff_nhds]
-    intro h
-    constructor
-    · rintro rfl
-      obtain ⟨x, hx⟩ := h (Iio 1) (Iio_mem_nhds zero_lt_one)
-      exact hx.2 <| lt_one_iff.mp hx.1.1
-    · intro p plt
-      obtain ⟨x, hx⟩ := h (Ioo p (o + 1)) <| Ioo_mem_nhds plt (lt_succ o)
-      use x
-      refine ⟨hx.1.2, ⟨hx.1.1.1, lt_of_le_of_ne ?_ hx.2⟩⟩
-      have := hx.1.1.2
-      rwa [← succ_eq_add_one, lt_succ_iff] at this
-  · rw [accPt_iff_nhds]
-    intro h u umem
-    obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds umem ⟨0, pos_iff_ne_zero.mpr h.1⟩
-    obtain ⟨x, hx⟩ := h.2 l hl.1
-    use x
-    exact ⟨⟨hl.2 ⟨hx.2.1, hx.2.2.le⟩, hx.1⟩, hx.2.2.ne⟩
+  apply SuccOrder.accPt_principal.trans
+  simp
 
+set_option linter.deprecated false in
+@[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
 theorem IsAcc.forall_lt {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) :
     ∀ p < o, (S ∩ Ioo p o).Nonempty := ((isAcc_iff _ _).mp h).2
 
+set_option linter.deprecated false in
+@[deprecated AccPt.not_isMin (since := "2026-05-24")]
 theorem IsAcc.pos {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) :
     0 < o := pos_iff_ne_zero.mpr ((isAcc_iff _ _).mp h).1
 
-theorem IsAcc.isSuccLimit {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : IsSuccLimit o := by
-  rw [isAcc_iff] at h
-  rw [isSuccLimit_iff]
-  refine ⟨h.1, isSuccPrelimit_of_succ_ne fun x hx ↦ ?_⟩
-  rcases h.2 x (lt_of_lt_of_le (lt_succ x) hx.le) with ⟨p, hp⟩
-  exact (hx.symm ▸ (succ_le_iff.mpr hp.2.1)).not_gt hp.2.2
+set_option linter.deprecated false in
+@[deprecated AccPt.isSuccLimit (since := "2026-05-24")]
+theorem IsAcc.isSuccLimit {o : Ordinal} {S : Set Ordinal} (h : o.IsAcc S) : IsSuccLimit o :=
+  AccPt.isSuccLimit h
 
-theorem IsAcc.mono {o : Ordinal} {S T : Set Ordinal} (h : S ⊆ T) (ho : o.IsAcc S) :
-    o.IsAcc T := by
-  rw [isAcc_iff] at *
-  exact ⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩
+set_option linter.deprecated false in
+@[deprecated AccPt.mono (since := "2026-05-24")]
+theorem IsAcc.mono {o : Ordinal} {S T : Set Ordinal} (h : S ⊆ T) (ho : o.IsAcc S) : o.IsAcc T :=
+  AccPt.mono ho (monotone_principal h)
 
+set_option linter.deprecated false in
+@[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
 theorem IsAcc.inter_Ioo_nonempty {o : Ordinal} {S : Set Ordinal} (hS : o.IsAcc S)
     {p : Ordinal} (hp : p < o) : (S ∩ Ioo p o).Nonempty := hS.forall_lt p hp
 
@@ -227,19 +217,27 @@ theorem accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) :
     AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S)) := by
   rw [← comap_principal, isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]
 
+set_option linter.deprecated false in
+@[deprecated isClosed_iff_accPt (since := "2026-05-24")]
 theorem isClosedBelow_iff {S : Set Ordinal} {o : Ordinal} : IsClosedBelow S o ↔
     ∀ p < o, IsAcc p S → p ∈ S := by
   simp [IsClosedBelow, IsAcc, isClosed_iff_accPt, ← comap_principal,
     isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]
 
+set_option linter.deprecated false in
+@[deprecated isClosed_iff_accPt (since := "2026-05-24")]
 alias ⟨IsClosedBelow.forall_lt, _⟩ := isClosedBelow_iff
 
+set_option linter.deprecated false in
+@[deprecated isClosed_sInter (since := "2026-05-24")]
 theorem IsClosedBelow.sInter {o : Ordinal} {S : Set (Set Ordinal)}
     (h : ∀ C ∈ S, IsClosedBelow C o) : IsClosedBelow (⋂₀ S) o := by
   rw [isClosedBelow_iff]
-  intro p plto pAcc C CmemS
-  exact (h C CmemS).forall_lt p plto (pAcc.mono (sInter_subset_of_mem CmemS))
+  exact fun p plto pAcc C CmemS ↦ (h C CmemS).forall_lt p plto <|
+    AccPt.mono pAcc (monotone_principal (sInter_subset_of_mem CmemS))
 
+set_option linter.deprecated false in
+@[deprecated isClosed_iInter (since := "2026-05-24")]
 theorem IsClosedBelow.iInter {ι : Type u} {f : ι → Set Ordinal} {o : Ordinal}
     (h : ∀ i, IsClosedBelow (f i) o) : IsClosedBelow (⋂ i, f i) o :=
   IsClosedBelow.sInter fun _ ⟨i, hi⟩ ↦ hi ▸ (h i)

Mathlib/Topology/Order/SuccPred.lean

@@ -20,7 +20,7 @@ public section
 variable {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α]
   {a : α} {s : Set α}
 
-open Order Topology
+open Filter Order Set Topology
 
 namespace SuccOrder
 variable [SuccOrder α]
@@ -42,10 +42,10 @@ 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))
+      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (mem_singleton a))
     refine ha.isSuccPrelimit l ?_
     rw [← succ_eq_iff_covBy]
-    simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂
+    simp only [mem_Ioo, 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
@@ -56,15 +56,44 @@ theorem isOpen_singleton_iff : IsOpen {a} ↔ ¬ IsSuccLimit a := by
 theorem nhds_eq_pure {a : α} : 𝓝 a = pure a ↔ ¬ IsSuccLimit a :=
   (isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff
 
+@[to_dual]
+theorem nhds_of_isMin {a : α} (h : IsMin a) : 𝓝 a = pure a := by
+  rw [nhds_eq_pure, isSuccLimit_iff]
+  tauto
+
+@[to_dual (attr := simp)]
+theorem nhds_bot [OrderBot α] : 𝓝 (⊥ : α) = pure ⊥ :=
+  nhds_of_isMin isMin_bot
+
 @[to_dual]
 theorem isOpen_iff {s : Set α} : IsOpen s ↔
-    ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s := by
+    ∀ o ∈ s, IsSuccLimit o → ∃ a < o, 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]
+  · rw [(hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff]
     grind
   · simp [nhds_eq_pure.2 ho', ho, ho']
 
+@[to_dual]
+theorem accPt_principal {a : α} {s : Set α} :
+    AccPt a (𝓟 s) ↔ ¬ IsMin a ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty := by
+  rw [accPt_iff_frequently]
+  by_cases ha : IsMin a
+  · simp [nhds_of_isMin, ha]
+  · rw [not_isMin_iff] at ha ⊢
+    simp_rw [(hasBasis_nhds_Ioc_of_exists_lt ha).frequently_iff, Set.Nonempty, mem_inter_iff]
+    grind
+
+@[to_dual]
+theorem _root_.AccPt.not_isMin {a : α} {s : Set α} (h : AccPt a (𝓟 s)) : ¬ IsMin a :=
+  (accPt_principal.1 h).1
+
+@[to_dual]
+theorem _root_.AccPt.isSuccLimit {a : α} {s : Set α} (h : AccPt a (𝓟 s)) : IsSuccLimit a := by
+  rw [isSuccLimit_iff, IsSuccPrelimit]
+  simp_rw [accPt_principal, Set.Nonempty] at h
+  grind [covBy_iff_Ioo_eq]
+
 @[to_dual]
 theorem isSuccLimit_of_mem_frontier {a : α} {s : Set α} (ha : a ∈ frontier s) : IsSuccLimit a := by
   rw [← isOpen_singleton_iff.not_left]