instTotallyDisconnectedSpaceUltrafilter

English

The space Ultrafilter α is totally disconnected; every connected subset is a singleton.

Русский

Пространство Ultrafilter α totally disconnected: каждая связная подмножество — одиночка.

LaTeX

$$"TotallyDisconnectedSpace\left(Ultrafilter\ α\right)"$$

Lean4

instance : TotallyDisconnectedSpace (Ultrafilter α) :=
  by
  rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
  intro A
  simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and]
  intro B hB
  rw [← Ultrafilter.coe_le_coe]
  intro s hs
  rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB
  let Z := {F : Ultrafilter α | s ∈ F}
  have hZ : IsClopen Z := ⟨ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩
  exact hB ⟨Z, hZ, hs⟩

Похожие утверждения