Theorems · Theorem · general topology

loc_compact_Haus_tot_disc_of_zero_dim

∀ {H : Type u_3} [inst : TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
  TopologicalSpace.IsTopologicalBasis {s | IsClopen s}

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

Defined in

Mathlib.Topology.Separation.Profinite

Cited by

2 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLocallyCompactSpaceT2SpaceTotallyDisconnectedSpace