Separation properties: profinite spaces

theorem totallySeparatedSpace_of_t0_of_basis_clopen {X : Type u_1} [TopologicalSpace X] [T0Space X] (h : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) : TotallySeparatedSpace X

A T0 space with a clopen basis is totally separated.

@[deprecated totallySeparatedSpace_of_t0_of_basis_clopen (since := "2025-09-11")]

theorem totallySeparatedSpace_of_t1_of_basis_clopen {X : Type u_1} [TopologicalSpace X] [T0Space X] (h : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) : TotallySeparatedSpace X

Alias of totallySeparatedSpace_of_t0_of_basis_clopen.

---

A T0 space with a clopen basis is totally separated.

theorem nhds_basis_clopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsClopen s) id

theorem isTopologicalBasis_isClopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

theorem compact_exists_isClopen_in_isOpen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] {x : X} {U : Set X} (is_open : IsOpen U) (memU : x ∈ U) : ∃ (V : Set X), IsClopen V ∧ x ∈ V ∧ V ⊆ U

Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set.

theorem loc_compact_Haus_tot_disc_of_zero_dim {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TopologicalSpace.IsTopologicalBasis {s : Set H | IsClopen s}

A locally compact Hausdorff totally disconnected space has a basis with clopen elements.

theorem loc_compact_t2_tot_disc_iff_tot_sep {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] : TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

A locally compact Hausdorff space is totally disconnected if and only if it is totally separated.

@[instance 100]

instance instTotallySeparatedSpaceOfTotallyDisconnectedSpace {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TotallySeparatedSpace H

A totally disconnected compact Hausdorff space is totally separated.