Theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open

Modification history

2024-05-28 13:06
Mathlib/Topology/Compactness/Compact.lean
feat(Topology): a profinite space has countably many clopens iff it is second countable (#12986)
Added eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_openView on Github →