RegularPairs.lean

1import BFPP.OrdinalCofinality2import BFPP.ClopenPairs3import BFPP.CountablePairs4import Mathlib.SetTheory.Cardinal.Regular56/-! # Regular uncountable ordinal lengths for the main realization -/78namespace BFPP910set_option autoImplicit false11open Set Order Cardinal1213universe u1415structure RegularOrdinalPair (K : Type u) [TopologicalSpace K] where16  positiveLength : Ordinal.{u}17  negativeLength : Ordinal.{u}18  positiveLimit : IsSuccLimit positiveLength19  negativeLimit : IsSuccLimit negativeLength20  positiveRegular : positiveLength.cof.ord = positiveLength21  negativeRegular : negativeLength.cof.ord = negativeLength22  families : @InseparablePair K (OrdinalIndex positiveLength) (OrdinalIndex negativeLength) _ _23    (@ordinalIndexOrderBot positiveLength ⟨positiveLimit⟩) _24    (@ordinalIndexOrderBot negativeLength ⟨negativeLimit⟩)2526variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [T2Space K]2728theorem exists_regularOrdinalPair (hF : IsFSpace K) (hED : ¬ ExtremallyDisconnected K) :29    Nonempty (RegularOrdinalPair K) := by30  by_cases hsep : TotallySeparatedSpace K31  · letI : TotallySeparatedSpace K := hsep32    obtain ⟨g⟩ := exists_clopen_chainGap hED33    obtain ⟨ρ, σ, hρ, hσ, hregρ, hregσ, g'⟩ := g.exists_indexedGap34    letI : Fact (IsSuccLimit ρ) := ⟨hρ⟩35    letI : Fact (IsSuccLimit σ) := ⟨hσ⟩36    exact ⟨⟨ρ, σ, hρ, hσ, hregρ, hregσ, g'.some.toInseparablePair⟩⟩37  · obtain ⟨ρ, hρ, hreg, F⟩ := exists_regular_pair_of_not_totallySeparated hF hsep38    exact ⟨⟨ρ, ρ, hρ, hρ, hreg, hreg, F.some⟩⟩3940theorem countable_ordinalIndex_of_card_le_aleph0 (ρ : Ordinal.{u}) (hρ : ρ.card ≤ ℵ₀) :41    Countable (OrdinalIndex ρ) := by42  apply Cardinal.mk_le_aleph0_iff.mp43  rw [Cardinal.mk_Iio_ordinal]44  simpa only [Cardinal.lift_aleph0] using Cardinal.lift_le.mpr hρ4546namespace RegularOrdinalPair4748noncomputable def length (R : RegularOrdinalPair K) : Ordinal.{u} := max R.positiveLength R.negativeLength4950theorem length_isLimit (R : RegularOrdinalPair K) : IsSuccLimit R.length := by51  rcases le_total R.positiveLength R.negativeLength with h | h52  · simpa only [length, max_eq_right h] using R.negativeLimit53  · simpa only [length, max_eq_left h] using R.positiveLimit5455theorem length_regular (R : RegularOrdinalPair K) : R.length.cof.ord = R.length := by56  rcases le_total R.positiveLength R.negativeLength with h | h57  · simpa only [length, max_eq_right h] using R.negativeRegular58  · simpa only [length, max_eq_left h] using R.positiveRegular5960theorem length_card_eq_cof (R : RegularOrdinalPair K) : R.length.card = R.length.cof := by61  have h := congrArg Ordinal.card R.length_regular62  simpa using h.symm6364theorem length_isInitial (R : RegularOrdinalPair K) : R.length.card.ord = R.length := by65  rw [R.length_card_eq_cof]66  exact R.length_regular6768theorem length_card_isRegular (R : RegularOrdinalPair K) : R.length.card.IsRegular := by69  rw [R.length_card_eq_cof]70  exact Cardinal.isRegular_cof R.length_isLimit7172theorem length_uncountable (R : RegularOrdinalPair K) (hF : IsFSpace K) : ℵ₀ < R.length.card := by73  by_contra h74  have hcount : R.length.card ≤ ℵ₀ := le_of_not_gt h75  have hp : R.positiveLength.card ≤ ℵ₀ :=76    (Ordinal.card_le_card (le_max_left _ _)).trans hcount77  have hn : R.negativeLength.card ≤ ℵ₀ :=78    (Ordinal.card_le_card (le_max_right _ _)).trans hcount79  letI : Fact (IsSuccLimit R.positiveLength) := ⟨R.positiveLimit⟩80  letI : Fact (IsSuccLimit R.negativeLength) := ⟨R.negativeLimit⟩81  letI : Countable (OrdinalIndex R.positiveLength) := countable_ordinalIndex_of_card_le_aleph0 _ hp82  letI : Countable (OrdinalIndex R.negativeLength) := countable_ordinalIndex_of_card_le_aleph0 _ hn83  exact R.families.false_of_countable_channels hF8485end RegularOrdinalPair86end BFPP

SHA-256