feat(SetTheory/Ordinal): fundamental sequences (leanprover-community#37019)

We redefine a fundamental sequence for an ordinal `o` as a strict monotonic function `Iio o.cof.ord → Iio o` with cofinal range. We reprove the API on the pre-existing predicate, and deprecate it.

Author: vihdzp

Mathlib.lean

@@ -6827,6 +6827,7 @@ public import Mathlib.SetTheory.Ordinal.Exponential
 public import Mathlib.SetTheory.Ordinal.Family
 public import Mathlib.SetTheory.Ordinal.FixedPoint
 public import Mathlib.SetTheory.Ordinal.FixedPointApproximants
+public import Mathlib.SetTheory.Ordinal.FundamentalSequence
 public import Mathlib.SetTheory.Ordinal.Notation
 public import Mathlib.SetTheory.Ordinal.Principal
 public import Mathlib.SetTheory.Ordinal.Rank

Mathlib/Order/Cofinal.lean

@@ -58,6 +58,7 @@ end LE
 section Preorder
 variable [Preorder α] [Preorder β]
 
+@[simp]
 theorem IsCofinal.univ : IsCofinal (@univ α) :=
   fun a ↦ ⟨a, ⟨⟩, le_rfl⟩
 
@@ -90,6 +91,10 @@ alias GaloisConnection.map_cofinal := GaloisConnection.map_isCofinal
 theorem OrderIso.map_isCofinal (e : α ≃o β) {s : Set α} (hs : IsCofinal s) : IsCofinal (e '' s) :=
   e.symm.to_galoisConnection.map_isCofinal hs
 
+@[simp]
+theorem OrderIso.map_isCofinal_iff (e : α ≃o β) {s : Set α} : IsCofinal (e '' s) ↔ IsCofinal s :=
+  ⟨fun hs ↦ by simpa using e.symm.map_isCofinal hs, e.map_isCofinal⟩
+
 @[deprecated (since := "2026-03-15")]
 alias OrderIso.map_cofinal := OrderIso.map_isCofinal
 

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -671,135 +671,6 @@ theorem bsup_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o
     (∀ i hi, f i hi < c) → bsup.{u, u} o f < c :=
   bsup_lt_ord_lift (by rwa [o.card.lift_id])
 
-/-! ### Fundamental sequences -/
-
--- TODO: move stuff about fundamental sequences to their own file.
-
-/-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
-    `a`. We provide `o` explicitly in order to avoid type rewrites. -/
-@[expose]
-def IsFundamentalSequence (a o : Ordinal.{u}) (f : ∀ b < o, Ordinal.{u}) : Prop :=
-  o ≤ a.cof.ord ∧ (∀ {i j} (hi hj), i < j → f i hi < f j hj) ∧ blsub.{u, u} o f = a
-
-namespace IsFundamentalSequence
-
-variable {a o : Ordinal.{u}} {f : ∀ b < o, Ordinal.{u}}
-
-protected theorem cof_eq (hf : IsFundamentalSequence a o f) : a.cof.ord = o :=
-  hf.1.antisymm' <| by
-    rw [← hf.2.2]
-    exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)
-
-protected theorem strict_mono (hf : IsFundamentalSequence a o f) {i j} :
-    ∀ hi hj, i < j → f i hi < f j hj :=
-  hf.2.1
-
-theorem blsub_eq (hf : IsFundamentalSequence a o f) : blsub.{u, u} o f = a :=
-  hf.2.2
-
-theorem ord_cof (hf : IsFundamentalSequence a o f) :
-    IsFundamentalSequence a a.cof.ord fun i hi => f i (hi.trans_le (by rw [hf.cof_eq])) := by
-  have H := hf.cof_eq
-  subst H
-  exact hf
-
-theorem id_of_le_cof (h : o ≤ o.cof.ord) : IsFundamentalSequence o o fun a _ => a :=
-  ⟨h, @fun _ _ _ _ => id, blsub_id o⟩
-
-protected theorem zero {f : ∀ b < (0 : Ordinal), Ordinal} : IsFundamentalSequence 0 0 f :=
-  ⟨by rw [cof_zero, ord_zero], @fun i _ hi => (not_lt_zero hi).elim, blsub_zero f⟩
-
-protected theorem succ : IsFundamentalSequence (succ o) 1 fun _ _ => o := by
-  refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
-  · rw [cof_succ, ord_one]
-  · rw [lt_one_iff_zero] at hi hj
-    rw [hi, hj] at h
-    exact h.false.elim
-
-protected theorem monotone (hf : IsFundamentalSequence a o f) {i j : Ordinal} (hi : i < o)
-    (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj := by
-  rcases lt_or_eq_of_le hij with (hij | rfl)
-  · exact (hf.2.1 hi hj hij).le
-  · rfl
-
-theorem trans {a o o' : Ordinal.{u}} {f : ∀ b < o, Ordinal.{u}} (hf : IsFundamentalSequence a o f)
-    {g : ∀ b < o', Ordinal.{u}} (hg : IsFundamentalSequence o o' g) :
-    IsFundamentalSequence a o' fun i hi =>
-      f (g i hi) (by rw [← hg.2.2]; apply lt_blsub) := by
-  refine ⟨?_, @fun i j _ _ h => hf.2.1 _ _ (hg.2.1 _ _ h), ?_⟩
-  · rw [hf.cof_eq]
-    exact hg.1.trans (ord_cof_le o)
-  · rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
-    · exact hf.2.2
-    · exact hg.2.2
-
-protected theorem lt {a o : Ordinal} {s : Π p < o, Ordinal}
-    (h : IsFundamentalSequence a o s) {p : Ordinal} (hp : p < o) : s p hp < a :=
-  h.blsub_eq ▸ lt_blsub s p hp
-
-end IsFundamentalSequence
-
-/-- Every ordinal has a fundamental sequence. -/
-theorem exists_fundamental_sequence (a : Ordinal.{u}) :
-    ∃ f, IsFundamentalSequence a a.cof.ord f := by
-  suffices h : ∃ o f, IsFundamentalSequence a o f by
-    rcases h with ⟨o, f, hf⟩
-    exact ⟨_, hf.ord_cof⟩
-  rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
-  rcases ord_eq ι with ⟨r, wo, hr⟩
-  let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
-  let hrr' : r' ↪r r := Subrel.relEmbedding _ _
-  haveI := hrr'.isWellOrder
-  refine
-    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
-      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
-  · rw [← hι, hr]
-  · change r (hrr'.1 _) (hrr'.1 _)
-    rwa [hrr'.2, @enum_lt_enum _ r']
-  · rw [← hf, lsub_le_iff]
-    intro i
-    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
-      rcases h with ⟨i', hi', hfg⟩
-      exact hfg.trans_lt (lt_blsub _ _ _)
-    by_cases! h : ∀ j, r j i → f j < f i
-    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
-      rw [bfamilyOfFamily'_typein]
-    · obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
-      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
-      · by_contra! H
-        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
-      · rwa [bfamilyOfFamily'_typein]
-
-theorem IsFundamentalSequence.of_isNormal {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f)
-    {a o} (ha : IsSuccLimit a) {g} (hg : IsFundamentalSequence a o g) :
-    IsFundamentalSequence (f a) o fun b hb => f (g b hb) := by
-  refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
-  · rcases exists_lsub_cof (f a) with ⟨ι, f', hf', hι⟩
-    rw [← hg.cof_eq, ord_le_ord, ← hι]
-    suffices (lsub.{u, u} fun i => sInf { b : Ordinal | f' i ≤ f b }) = a by
-      rw [← this]
-      apply cof_lsub_le
-    have H : ∀ i, ∃ b < a, f' i ≤ f b := fun i => by
-      have := lt_lsub.{u, u} f' i
-      rw [hf', ← IsNormal.blsub_eq.{u, u} hf ha, lt_blsub_iff] at this
-      simpa using this
-    refine (lsub_le fun i => ?_).antisymm (le_of_forall_lt fun b hb => ?_)
-    · rcases H i with ⟨b, hb, hb'⟩
-      exact lt_of_le_of_lt (csInf_le' hb') hb
-    · have := hf.strictMono hb
-      rw [← hf', lt_lsub_iff] at this
-      obtain ⟨i, hi⟩ := this
-      rcases H i with ⟨b, _, hb⟩
-      exact
-        ((le_csInf_iff'' ⟨b, by exact hb⟩).2 fun c hc =>
-          hf.strictMono.le_iff_le.1 (hi.trans hc)).trans_lt (lt_lsub _ i)
-  · rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
-        hg.2.2]
-    exact IsNormal.blsub_eq.{u, u} hf ha
-
-@[deprecated (since := "2025-12-25")]
-alias IsNormal.isFundamentalSequence := IsFundamentalSequence.of_isNormal
-
 @[simp]
 theorem cof_add (a b : Ordinal) : b ≠ 0 → cof (a + b) = cof b := fun h => by
   rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)