OrdinalCofinality.lean

1import BFPP.CofinalReindexing2import BFPP.SignRealization3import Mathlib.SetTheory.Ordinal.FundamentalSequence45/-! # Regular cofinal lengths for the sign construction -/67namespace BFPP89set_option autoImplicit false10open Set Order1112universe u1314theorem exists_ordinal_cofinal_from_bot (τ : Ordinal.{u}) [hτ : Fact (IsSuccLimit τ)] :15    ∃ ρ : Ordinal.{u}, ∃ hρ : IsSuccLimit ρ, ρ.cof.ord = ρ ∧16      ∃ φ : Iio ρ → Iio τ, Monotone φ ∧ φ ⟨0, hρ.pos⟩ = ⊥ ∧ IsCofinal (range φ) := by17  classical18  let ρ := τ.cof.ord19  have hρ : IsSuccLimit ρ := by20    apply Ordinal.one_lt_cof_iff.mp21    change 1 < τ.cof.ord.cof22    rw [Ordinal.cof_ord_cof]23    exact Ordinal.one_lt_cof_iff.mpr hτ.out24  have hreg : ρ.cof.ord = ρ := by simp [ρ]25  obtain ⟨f, hf⟩ := Ordinal.exists_isFundamentalSeq (o := τ) (a := ρ) rfl26  letI : Fact (IsSuccLimit ρ) := ⟨hρ⟩27  let φ : Iio ρ → Iio τ := fun i => if i.val = 0 then ⊥ else f i28  refine ⟨ρ, hρ, hreg, φ, ?_, ?_, ?_⟩29  · intro i j hij30    by_cases hi : i.val = 031    · simp only [φ, if_pos hi]32      exact bot_le33    · have hj : j.val ≠ 0 := by34        intro hj35        exact hi (le_antisymm (hj ▸ hij) bot_le)36      simpa only [φ, if_neg hi, if_neg hj] using hf.strictMono.monotone hij37  · simp [φ]38  · intro a39    obtain ⟨_, ⟨i, rfl⟩, hai⟩ := hf.isCofinal_range a40    obtain ⟨j, hij⟩ := exists_gt i41    have hj : j.val ≠ 0 := ne_of_gt (lt_of_le_of_lt bot_le hij)42    refine ⟨φ j, mem_range_self j, ?_⟩43    simpa only [φ, if_neg hj] using hai.trans (hf.strictMono hij).le4445variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [T2Space K]4647theorem exists_regular_pair_of_not_totallySeparated (hF : IsFSpace K)48    (hK : ¬ TotallySeparatedSpace K) :49    ∃ ρ : Ordinal.{u}, ∃ hρ : IsSuccLimit ρ, ρ.cof.ord = ρ ∧50      @Nonempty (@InseparablePair K (OrdinalIndex ρ) (OrdinalIndex ρ) _ _51        (@ordinalIndexOrderBot ρ ⟨hρ⟩) _ (@ordinalIndexOrderBot ρ ⟨hρ⟩)) := by52  obtain ⟨p, q, hpq, hinsep⟩ := exists_clopenInseparable_of_not_totallySeparated hK53  have hd : Disjoint (closure ({p} : Set K)) (closure ({q} : Set K)) := by54    simpa only [isClosed_singleton.closure_eq, disjoint_singleton] using hpq55  obtain ⟨seed, hp, hq⟩ := exists_sign_extension ({p} : Set K) {q} hd56  obtain ⟨d, hlimit, hd, hbefore⟩ := exists_first_bad_limit hF seed p q hinsep57    (hp p (subset_closure (mem_singleton p))) (hq q (subset_closure (mem_singleton q)))58  letI : Fact (IsSuccLimit d) := ⟨hlimit⟩59  let F := (stoppedSignChain seed d hd hbefore).toInseparablePair60  obtain ⟨ρ, hρ, hreg, φ, hφ, hφ₀, hcof⟩ := exists_ordinal_cofinal_from_bot d61  letI : Fact (IsSuccLimit ρ) := ⟨hρ⟩62  exact ⟨ρ, hρ, hreg, ⟨F.reindex φ φ hφ hφ hφ₀ hφ₀ hcof hcof⟩⟩6364end BFPP

SHA-256