ClopenCompleteness.lean

1import BFPP.BooleanGap2import Mathlib.Topology.ExtremallyDisconnected3import Mathlib.Topology.Separation.Profinite4import Mathlib.Topology.Sets.Closeds56/-! # Completeness of clopens detects extremal disconnectedness -/78namespace BFPP910set_option autoImplicit false11open Set TopologicalSpace1213variable {K : Type*} [TopologicalSpace K] [CompactSpace K] [T2Space K]14  [TotallyDisconnectedSpace K]1516theorem extremallyDisconnected_of_clopen_complete17    (h : ∀ S : Set (Clopens K), ∃ H, IsLUB S H) : ExtremallyDisconnected K := by18  classical19  refine ⟨fun U hU => ?_⟩20  let S : Set (Clopens K) := {C | (C : Set K) ⊆ U}21  obtain ⟨H, hH⟩ := h S22  have hUH : U ⊆ H := by23    intro t ht24    obtain ⟨V, hV, htV, hVU⟩ := compact_exists_isClopen_in_isOpen hU ht25    exact hH.1 (show (⟨V, hV⟩ : Clopens K) ∈ S from hVU) htV26  have hcH : closure U ⊆ H := closure_minimal hUH H.isClosed27  have hHc : (H : Set K) ⊆ closure U := by28    intro t ht29    by_contra htc30    obtain ⟨V, hV, htV, hVc⟩ := compact_exists_isClopen_in_isOpen31      isClosed_closure.isOpen_compl htc32    let V' : Clopens K := ⟨V, hV⟩33    have hub : H ⊓ V'ᶜ ∈ upperBounds S := by34      intro C hC35      refine le_inf (hH.1 hC) ?_36      intro x hx hxV37      exact hVc hxV (subset_closure (hC hx))38    have hle := hH.2 hub39    have ht' : t ∈ H ⊓ V'ᶜ := hle ht40    exact ht'.2 htV41  have he : closure U = (H : Set K) := hcH.antisymm hHc42  rw [he]43  exact H.isOpen4445theorem exists_clopen_chainGap (h : ¬ ExtremallyDisconnected K) :46    Nonempty (ChainGap (Clopens K)) := by47  classical48  apply exists_chainGap49  by_contra hn50  apply h51  apply extremallyDisconnected_of_clopen_complete52  intro S53  by_contra hS54  exact hn ⟨S, hS⟩5556end BFPP

SHA-256