PointwiseSupremum.lean

1import BFPP.OrdinalIndex2import Mathlib.Topology.UnitInterval3import Mathlib.Order.CompleteLatticeIntervals4import Mathlib.Topology.UrysohnsLemma5import Mathlib.Topology.ExtremallyDisconnected67/-! # Discontinuous pointwise suprema and cardinal minimality -/89namespace BFPP1011set_option autoImplicit false12open Set Order Cardinal unitInterval1314universe u15variable {K : Type u} [TopologicalSpace K]1617noncomputable def pointwiseSup (S : Set C(K, I)) (t : K) : I := ⨆ f ∈ S, f t1819theorem pointwiseSup_mono {S T : Set C(K, I)} (h : S ⊆ T) : pointwiseSup S ≤ pointwiseSup T := by20  intro t21  exact iSup_le fun f => iSup_le fun hf => le_iSup_of_le f (le_iSup_of_le (h hf) le_rfl)2223theorem pointwiseSup_finite (S : Set C(K, I)) (hS : S.Finite) : Continuous (pointwiseSup S) := by24  induction S, hS using Set.Finite.induction_on with25  | empty =>26    have he : pointwiseSup (∅ : Set C(K, I)) = fun _ : K => (⊥ : I) := by27      funext t28      simp [pointwiseSup]29    rw [he]30    exact continuous_const31  | @insert f S hf hS ih =>32    have he : pointwiseSup (insert f S) = fun t => f t ⊔ pointwiseSup S t := by33      funext t34      apply le_antisymm35      · refine iSup_le fun g => iSup_le fun hg => ?_36        rcases hg with rfl | hg37        · exact le_sup_left38        · have hh : g t ≤ pointwiseSup S t := le_iSup_of_le g (le_iSup_of_le hg le_rfl)39          exact hh.trans le_sup_right40      · apply sup_le41        · exact le_iSup_of_le f (le_iSup_of_le (mem_insert f S) le_rfl)42        · exact pointwiseSup_mono (subset_insert f S) t43    rw [he]44    exact f.continuous.sup ih4546def supportedUnitFunctions (U : Set K) : Set C(K, I) := {f | ∀ t, t ∉ U → f t = 0}4748theorem pointwiseSup_supported_eq [CompactSpace K] [T2Space K] (U : Set K) (hU : IsOpen U) :49    pointwiseSup (supportedUnitFunctions U) = U.indicator (fun _ => (1 : I)) := by50  classical51  funext t52  by_cases ht : t ∈ U53  · rw [indicator_of_mem ht]54    apply top_unique55    obtain ⟨f, hf₀, hf₁, hb⟩ := exists_continuous_zero_one_of_isClosed hU.isClosed_compl56      (isClosed_singleton (x := t)) (by57        rw [disjoint_singleton_right]58        simpa only [mem_compl_iff, not_not] using ht)59    let g : C(K, I) := ⟨fun x => ⟨f x, hb x⟩, f.continuous.subtype_mk _⟩60    have hg : g ∈ supportedUnitFunctions U := by61      intro x hx62      apply Subtype.ext63      exact hf₀ hx64    have hgt : g t = 1 := Subtype.ext (hf₁ (mem_singleton t))65    change (1 : I) ≤ ⨆ f ∈ supportedUnitFunctions U, f t66    rw [← hgt]67    exact le_iSup_of_le g (le_iSup_of_le hg le_rfl)68  · rw [indicator_of_notMem ht]69    apply bot_unique70    exact iSup_le fun f => iSup_le fun hf => (hf t ht).le7172theorem exists_discontinuous_pointwiseSup [CompactSpace K] [T2Space K]73    (U : Set K) (hU : IsOpen U) (hclosed : ¬ IsClosed U) :74    ∃ S : Set C(K, I), ¬ Continuous (pointwiseSup S) := by75  refine ⟨supportedUnitFunctions U, ?_⟩76  intro hc77  apply hclosed78  have he : (pointwiseSup (supportedUnitFunctions U)) ⁻¹' {1} = U := by79    rw [pointwiseSup_supported_eq U hU]80    ext t81    by_cases ht : t ∈ U <;> simp [ht]82  rw [← he]83  exact isClosed_singleton.preimage hc8485theorem exists_open_not_closed_of_not_ED (hK : ¬ ExtremallyDisconnected K) :86    ∃ U : Set K, IsOpen U ∧ ¬ IsClosed U := by87  by_contra h88  have hall : ∀ U : Set K, IsOpen U → IsClosed U := by89    intro U hU90    by_contra hclosed91    exact h ⟨U, hU, hclosed⟩92  apply hK93  exact ⟨fun U hU => by rw [(hall U hU).closure_eq]; exact hU⟩9495/-- Minimality is with respect to cardinality, not inclusion or ordinal length. -/96theorem exists_minimal_discontinuous_family [CompactSpace K] [T2Space K]97    (U : Set K) (hU : IsOpen U) (hclosed : ¬ IsClosed U) :98    ∃ S : Set C(K, I), ¬ Continuous (pointwiseSup S) ∧ ℵ₀ ≤ #S ∧99      ∀ T : Set C(K, I), #T < #S → Continuous (pointwiseSup T) := by100  obtain ⟨S, hS, hmin⟩ := (InvImage.wf (fun S : Set C(K, I) => #S) Cardinal.lt_wf).has_min101    {S | ¬ Continuous (pointwiseSup S)} (exists_discontinuous_pointwiseSup U hU hclosed)102  refine ⟨S, hS, ?_, ?_⟩103  · by_contra h104    have hfin : Finite S := Cardinal.lt_aleph0_iff_finite.mp (lt_of_not_ge h)105    exact hS (pointwiseSup_finite S (Set.toFinite S))106  · intro T hT107    by_contra hc108    exact hmin T hc hT109110end BFPP

SHA-256