CofinalSequences.lean

1import BFPP.OrdinalIndex2import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal34/-! # Cofinal sequences indexed by regular limit ordinals -/56namespace BFPP78set_option autoImplicit false9open Set Order Ordinal Cardinal1011universe u12variable (A : Type u) [LinearOrder A] [Nonempty A] [NoMaxOrder A]1314theorem exists_regular_cofinal_sequence :15    ∃ τ : Ordinal.{u}, IsSuccLimit τ ∧ τ.cof.ord = τ ∧16      ∃ f : Iio τ → A, StrictMono f ∧ IsCofinal (range f) := by17  classical18  let R : Set A := {a | ∀ b, WellOrderingRel b a → b < a}19  have hR : IsCofinal R := isCofinal_setOfPred_imp_lt WellOrderingRel20  have hrel : ∀ a b : R, a < b → WellOrderingRel a.val b.val := by21    intro a b hab22    rcases trichotomous_of WellOrderingRel a.val b.val with hr | heq | hr23    · exact hr24    · exact (ne_of_lt hab (Subtype.ext heq)).elim25    · exact ((a.property b.val hr).not_gt hab).elim26  letI : WellFoundedLT R := ⟨(InvImage.wf Subtype.val WellOrderingRel.isWellOrder.wf).mono27    (fun {a b} hab => hrel a b hab)⟩28  letI : Nonempty R := hR.nonempty.to_subtype29  letI : NoMaxOrder R := ⟨by30    intro a31    obtain ⟨b, hab⟩ := exists_gt a.val32    obtain ⟨c, hc, hbc⟩ := hR b33    exact ⟨⟨c, hc⟩, hab.trans_le hbc⟩⟩34  obtain ⟨S, hS, htype⟩ := Ordinal.exists_ord_cof_eq R35  letI : Nonempty S := hS.nonempty.to_subtype36  letI : NoMaxOrder S := ⟨by37    intro a38    obtain ⟨b, hab⟩ := exists_gt a.val39    obtain ⟨c, hc, hbc⟩ := hS b40    exact ⟨⟨c, hc⟩, hab.trans_le hbc⟩⟩41  let τ := typeLT S42  have hlimit : IsSuccLimit τ := by43    apply Ordinal.one_lt_cof_iff.mp44    rw [Ordinal.cof_type]45    exact Order.one_lt_cof46  have hregular : τ.cof.ord = τ := by47    change (typeLT S).cof.ord = typeLT S48    rw [htype, Order.cof_ord_cof]49  let e : Iio τ ≃o S := OrderIso.ofRelIsoLT (Ordinal.enum (α := S) (· < ·))50  let f : Iio τ → A := fun i => (e i).val.val51  refine ⟨τ, hlimit, hregular, f, ?_, ?_⟩52  · intro i j hij53    exact e.strictMono hij54  · intro a55    obtain ⟨b, hb, hab⟩ := hR a56    obtain ⟨c, hc, hbc⟩ := hS ⟨b, hb⟩57    refine ⟨c.val, ⟨e.symm ⟨c, hc⟩, ?_⟩, hab.trans hbc⟩58    simp [f]5960variable [OrderBot A]6162theorem exists_regular_cofinal_sequence_from_bot :63    ∃ τ : Ordinal.{u}, ∃ hτ : IsSuccLimit τ, τ.cof.ord = τ ∧64      ∃ f : Iio τ → A, Monotone f ∧ f ⟨0, hτ.pos⟩ = ⊥ ∧ IsCofinal (range f) := by65  classical66  obtain ⟨τ, hτ, hreg, f, hf, hcof⟩ := exists_regular_cofinal_sequence A67  let g : Iio τ → A := fun i => if i.val = 0 then ⊥ else f i68  refine ⟨τ, hτ, hreg, g, ?_, ?_, ?_⟩69  · intro i j hij70    by_cases hi : i.val = 071    · simp only [g, if_pos hi]72      exact bot_le73    · have hj : j.val ≠ 0 := by74        intro hj75        exact hi (le_antisymm (hj ▸ hij) bot_le)76      simpa only [g, if_neg hi, if_neg hj] using hf.monotone hij77  · simp [g]78  · intro a79    obtain ⟨_, ⟨i, rfl⟩, hai⟩ := hcof a80    obtain ⟨j, hij⟩ := hτ.isSuccPrelimit.noMaxOrder_Iio.exists_gt i81    have hj : j.val ≠ 0 := ne_of_gt (lt_of_le_of_lt bot_le hij)82    refine ⟨g j, mem_range_self j, ?_⟩83    simpa only [g, if_neg hj] using hai.trans (hf hij).le8485end BFPP

SHA-256