feat: TotallySeparatedSpace instance for profinite sets (#6722)

Adds an instance `TotallySeparatedSpace` for totally disconnected compact Hausdorff spaces. This direction of `compact_t2_tot_disc_iff_tot_sep` was missing an instance.
leanprover-community · Aug 23, 2023 · 77823cd · 77823cd
1 parent 552f9b5
commit 77823cd
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean
@@ -1984,6 +1984,9 @@ theorem compact_t2_tot_disc_iff_tot_sep : TotallyDisconnectedSpace α ↔ Totall
 
 variable [TotallyDisconnectedSpace α]
 
+/-- A totally disconnected compact Hausdorff space is totally separated. -/
+instance : TotallySeparatedSpace α := compact_t2_tot_disc_iff_tot_sep.mp inferInstance
+
 theorem nhds_basis_clopen (x : α) : (𝓝 x).HasBasis (fun s : Set α => x ∈ s ∧ IsClopen s) id :=
   ⟨fun U => by
     constructor