Theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open

Modification history

2025-04-07 16:11
Mathlib/Topology/Compactness/Bases.lean
chore: split IsTopologicalBasis results out of Compactness.Compact (#23401) …
Modified eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_openView on Github →
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 →