English
A totally disconnected compact Hausdorff space is totally separated.
Русский
Компактное хаусдорфово полностью несвязное пространство полностью раздельно.
LaTeX
$$$\\text{TotallyDisconnectedSpace } H \\Rightarrow \\text{TotallySeparatedSpace } H$$$
Lean4
/-- A locally compact Hausdorff totally disconnected space has a basis with clopen elements. -/
theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] :
IsTopologicalBasis {s : Set H | IsClopen s} :=
by
refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_
obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU
let u : Set s := ((↑) : s → H) ⁻¹' interior s
have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val
lift x to s using interior_subset xs
haveI : CompactSpace s := isCompact_iff_compactSpace.1 comp
obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs
have VisClopen' : IsClopen (((↑) : s → H) '' V) :=
by
refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1, ?_⟩
let v : Set u := ((↑) : u → s) ⁻¹' V
have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal
have f1 : IsOpenEmbedding ((↑) : u → H) := by
refine ⟨f0, ?_⟩
· have : Set.range ((↑) : u → H) = interior s :=
by
rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
apply Set.inter_eq_self_of_subset_right interior_subset
rw [this]
apply isOpen_interior
have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val
have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
rw [f3]
apply f1.isOpenMap v f2
use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU
