ClopenPairs.lean

1import BFPP.IndexedGaps2import BFPP.ClopenCompleteness34/-! # Inseparable continuous families obtained from clopen gaps -/56namespace BFPP78set_option autoImplicit false9open Set TopologicalSpace1011universe u v w12variable {K : Type u} [TopologicalSpace K]13  {ι : Type v} {κ : Type w} [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1415noncomputable def clopenStep (C : Clopens K) : C(K, ℝ) :=16  ⟨(C : Set K).indicator (fun _ => 1), C.isClopen.continuous_indicator continuous_const⟩1718@[simp] theorem clopenStep_apply (C : Clopens K) (t : K) [Decidable (t ∈ C)] :19    clopenStep C t = if t ∈ C then 1 else 0 := by20  classical21  change (C : Set K).indicator (fun _ => (1 : ℝ)) t = _22  by_cases h : t ∈ C <;> simp [Set.indicator, h]2324noncomputable def clopenFamily (F : ι → Clopens K) (hm : Monotone F) (h₀ : F ⊥ = ⊥) :25    IncreasingFamily K ι where26  functions := fun i => clopenStep (F i)27  monotone t := by28    classical29    intro i j hij30    by_cases hi : t ∈ F i31    · have hj := hm hij hi32      simp [hi, hj]33    · simp only [clopenStep_apply, if_neg hi]34      split_ifs <;> norm_num35  bounds i t := by36    classical37    simp only [clopenStep_apply]38    split_ifs <;> norm_num39  at_bot := by40    classical41    ext t42    simp [h₀, clopenStep]4344@[simp] theorem clopenFamily_levels (F : ι → Clopens K) (hm : Monotone F) (h₀ : F ⊥ = ⊥)45    (i : ι) : (clopenFamily F hm h₀).levels i = (F i : Set K) := by46  classical47  ext t48  change (if t ∈ F i then (1 : ℝ) else 0) = 1 ↔ t ∈ F i49  by_cases h : t ∈ F i <;> simp [h]5051namespace IndexedGap5253variable [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]5455noncomputable def toInseparablePair (g : IndexedGap (Clopens K) ι κ) :56    InseparablePair K ι κ where57  positive := clopenFamily g.lower g.lower_mono g.lower_bot58  negative := clopenFamily (fun j => (g.upper j)ᶜ)59    (fun _ _ hij => compl_le_compl (g.upper_anti hij)) (by rw [g.upper_bot, compl_top])60  orthogonal i j t := by61    classical62    change clopenStep (g.lower i) t * clopenStep (g.upper j)ᶜ t = 063    by_cases ht : t ∈ g.lower i64    · have ht' : t ∈ g.upper j := g.cross i j ht65      have ht'' : t ∉ (g.upper j)ᶜ := fun h => h ht'66      simp [ht, ht'']67    · simp [ht]68  inseparable := by69    classical70    simp only [clopenFamily_levels]71    apply Set.not_disjoint_iff.mp72    intro hd73    have hd' : Disjoint (closure (⋃ i, (g.lower i : Set K)))74        (closure (⋃ j, ((g.upper j)ᶜ : Set K))) := by75      refine hd.mono le_rfl (closure_mono ?_)76      intro t ht77      obtain ⟨j, hj⟩ := mem_iUnion.mp ht78      refine mem_iUnion.mpr ⟨j, ?_⟩79      change clopenStep (g.upper j)ᶜ t = 180      rw [clopenStep_apply]81      exact if_pos (show t ∈ (g.upper j)ᶜ from hj)82    obtain ⟨C, hC, hUC, hCV⟩ := exists_clopen_of_closed_subset_open isClosed_closure83      isClosed_closure.isOpen_compl (Set.disjoint_left.mp hd')84    apply g.no_interpolant85    refine ⟨⟨C, hC⟩, ?_, ?_⟩86    · intro i t ht87      exact hUC (subset_closure (mem_iUnion.mpr ⟨i, ht⟩))88    · intro j t ht89      by_contra hn90      exact hCV ht (subset_closure (mem_iUnion.mpr ⟨j, hn⟩))9192end IndexedGap9394theorem not_hasBFPP_of_zeroDimensional_not_ED95    [CompactSpace K] [T2Space K] [TotallyDisconnectedSpace K]96    (h : ¬ ExtremallyDisconnected K) : ¬ HasBFPP C(K, ℝ) := by97  obtain ⟨g⟩ := exists_clopen_chainGap h98  obtain ⟨ρ, σ, hρ, hσ, _, _, g'⟩ := g.exists_indexedGap99  letI : Fact (Order.IsSuccLimit ρ) := ⟨hρ⟩100  letI : Fact (Order.IsSuccLimit σ) := ⟨hσ⟩101  exact g'.some.toInseparablePair.not_hasBFPP102103end BFPP

SHA-256