TerminalSupremum.lean

1import BFPP.PointwisePrefixes23/-! # An infinite initial ordinal with a discontinuous terminal pointwise supremum -/45namespace BFPP67set_option autoImplicit false8open Set Order Cardinal unitInterval910universe u11variable {K : Type u} [TopologicalSpace K] [CompactSpace K] [T2Space K]1213/-- The appendix construction only needs an open set which is not closed.14The codomain `I` is the actual closed real interval `[0,1]`. -/15theorem exists_terminal_pointwise_supremum (U : Set K) (hU : IsOpen U) (hclosed : ¬ IsClosed U) :16    ∃ η : Cardinal.{u}, ℵ₀ ≤ η ∧ ∃ hη : IsSuccLimit η.ord,17      ∃ (s : OrdinalIndex η.ord → C(K, I)) (sstar : K → I),18        Monotone (fun i t => s i t) ∧ s ⟨0, hη.pos⟩ = 0 ∧19        (∀ i : OrdinalIndex η.ord, IsSuccLimit i.val → ∀ t,20          s i t = ⨆ j : Iio i, s j.val t) ∧21        (∀ t, sstar t = ⨆ i, s i t) ∧ ¬ Continuous sstar := by22  classical23  obtain ⟨S, hS, hinf, hmin⟩ := exists_minimal_discontinuous_family U hU hclosed24  let η : Cardinal.{u} := #S25  have hη : IsSuccLimit η.ord := Cardinal.isSuccLimit_ord hinf26  letI : Fact (IsSuccLimit η.ord) := ⟨hη⟩27  let e : η.ord.ToType ≃ S := (Cardinal.eq.mp (by simp [η])).some28  let eo : OrdinalIndex η.ord ≃o η.ord.ToType := Ordinal.ToType.mk29  let g : η.ord.ToType → C(K, I) := fun i => (e i).val30  let go : OrdinalIndex η.ord → C(K, I) := g ∘ eo31  have hcont : ∀ i : η.ord.ToType, Continuous (pointwisePrefix g i) := by32    intro i33    rw [pointwisePrefix_image]34    apply hmin35    have hi : #(Iio i) < η := by36      simpa only [Cardinal.mk_ord_toType] using37        (Cardinal.mk_Iio_lt i (by simp))38    exact Cardinal.mk_image_le.trans_lt hi39  let s : OrdinalIndex η.ord → C(K, I) := fun i => ⟨pointwisePrefix g (eo i), hcont (eo i)⟩40  have hs : ∀ i, (s i : K → I) = pointwisePrefix go i := by41    intro i42    exact (pointwisePrefix_reindex eo g i).symm43  have htotal : ∀ t, (⨆ i, go i t) = pointwiseSup S t := by44    intro t45    apply le_antisymm46    · refine iSup_le fun i => ?_47      exact le_iSup_of_le (go i) (le_iSup_of_le (e (eo i)).property le_rfl)48    · refine iSup_le fun f => iSup_le fun hf => ?_49      obtain ⟨j, hj⟩ := e.surjective ⟨f, hf⟩50      obtain ⟨i, hi⟩ := eo.surjective j51      exact le_iSup_of_le i (by simp [go, g, Function.comp_def, hi, hj])52  refine ⟨η, hinf, hη, s, pointwiseSup S, ?_, ?_, ?_, ?_, hS⟩53  · intro i j hij t54    change s i t ≤ s j t55    rw [show s i t = pointwisePrefix go i t from congrFun (hs i) t,56      show s j t = pointwisePrefix go j t from congrFun (hs j) t]57    exact pointwisePrefix_mono go hij t58  · apply ContinuousMap.ext59    intro t60    have hz := congrFun (pointwisePrefix_bot go) t61    exact (congrFun (hs ⟨0, hη.pos⟩) t).trans hz62  · intro i hi t63    have hbetween : ∀ j : OrdinalIndex η.ord, j < i → ∃ k, j < k ∧ k < i := by64      intro j hj65      have hji : j.val < i.val := hj66      have hsucc : succ j.val < i.val := hi.succ_lt hji67      exact ⟨⟨succ j.val, hsucc.trans i.property⟩, Order.lt_succ j.val, hsucc⟩68    calc69      s i t = pointwisePrefix go i t := congrFun (hs i) t70      _ = ⨆ j : Iio i, pointwisePrefix go j.val t := pointwisePrefix_limit go i hbetween t71      _ = ⨆ j : Iio i, s j.val t := by72        apply iSup_congr73        intro j74        exact (congrFun (hs j.val) t).symm75  · intro t76    calc77      pointwiseSup S t = ⨆ i, go i t := (htotal t).symm78      _ = ⨆ i, pointwisePrefix go i t := (pointwisePrefix_terminal go t).symm79      _ = ⨆ i, s i t := by80        apply iSup_congr81        intro i82        exact (congrFun (hs i) t).symm8384theorem exists_terminal_pointwise_supremum_of_not_ED (hK : ¬ ExtremallyDisconnected K) :85    ∃ η : Cardinal.{u}, ℵ₀ ≤ η ∧ ∃ hη : IsSuccLimit η.ord,86      ∃ (s : OrdinalIndex η.ord → C(K, I)) (sstar : K → I),87        Monotone (fun i t => s i t) ∧ s ⟨0, hη.pos⟩ = 0 ∧88        (∀ i : OrdinalIndex η.ord, IsSuccLimit i.val → ∀ t,89          s i t = ⨆ j : Iio i, s j.val t) ∧90        (∀ t, sstar t = ⨆ i, s i t) ∧ ¬ Continuous sstar := by91  obtain ⟨U, hU, hc⟩ := exists_open_not_closed_of_not_ED hK92  exact exists_terminal_pointwise_supremum U hU hc9394end BFPP

SHA-256