Theorems · Theorem · general topology
loc_compact_t2_tot_disc_iff_tot_sep
∀ {H : Type u_3} [inst : TopologicalSpace H] [LocallyCompactSpace H] [T2Space H],
TotallyDisconnectedSpace H ↔ TotallySeparatedSpace HA locally compact Hausdorff space is totally disconnected if and only if it is totally separated.
- Defined in
- Mathlib.Topology.Separation.Profinite
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- T2Spacestatement and proof · cited by 1,351
- LocallyCompactSpacestatement and proof · cited by 324
- TotallyDisconnectedSpacestatement and proof · cited by 295
- TotallySeparatedSpacestatement · cited by 9
- loc_compact_Haus_tot_disc_of_zero_dimproof · cited by 2
- totallySeparatedSpace_of_t0_of_basis_clopenproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.