Commit 2024-05-28 13:06 8d633f39

View on Github →

feat(Topology): a profinite space has countably many clopens iff it is second countable (#12986)

Estimated changes

Modified Mathlib/Topology/ClopenBox.lean

added theorem TopologicalSpace.Clopens.countable_iff_second_countable

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open

added theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open