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.

theorem exists_clopen_of_closed_subset_open {X : Type u_4} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] {Z U : Set X} (hZ : IsClosed Z) (hU : IsOpen U) (hZU : Z ⊆ U) : ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

In a totally disconnected compact Hausdorff space X, if Z ⊆ U are subsets with Z closed and U open, there exists a clopen C with Z ⊆ C ⊆ U.

theorem exists_clopen_partition_of_clopen_cover {X : Type u_4} {I : Type u_5} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [Finite I] {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i)) (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : Set.univ.PairwiseDisjoint Z) : ∃ (C : I → Set X), (∀ (i : I), IsClopen (C i)) ∧ (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ (i : I), D i ⊆ ⋃ (i : I), C i ∧ Set.univ.PairwiseDisjoint C

Let X be a totally disconnected compact Hausdorff space, D i ⊆ X a finite family of clopens, and Z i ⊆ D i closed. Assume that the Z i are pairwise disjoint. Then there exist clopens Z i ⊆ C i ⊆ D i with the C i disjoint, and such that ∪ D i ⊆ ∪ C i.