Theorem TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen

Modification history

2025-09-11 07:52
Mathlib/Topology/Bases.lean
feat: the topology on WithTop is second countable (#29466)
Added TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpenView on Github →