Theorem zeroDimensionalSpace_iff_nhds_hasBasis_isClopen

Modification history

2026-10-08 14:19
Mathlib/Topology/InductiveDimension/Classes.lean
feat: zero-dimensional spaces (#40901) …
Added zeroDimensionalSpace_iff_nhds_hasBasis_isClopenView on Github →