Commit 2026-10-08 14:19 cb08acac

feat: zero-dimensional spaces (#40901) We introduce an abbreviation ZeroDimensionalSpace X = HasSmallInductiveDimensionLT 1. We prove, in various forms, the characterization of these spaces as those that have a basis of clopen sets. We then use this to restate or generalize various results throughout the library, which were formerly writing down the IsTopologicalBasis {X | IsClopen X} condition in full.