Commit 2023-12-29 07:09 b8c97409

View on Github →

feat(Topology): clopen subsets of products of compact spaces are unions of clopen boxes (#8678)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ClopenBox.lean

added theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod

added theorem TopologicalSpace.Clopens.exists_prod_subset

added theorem TopologicalSpace.Clopens.surjective_finset_sup_prod

Modified Mathlib/Topology/CompactOpen.lean

added theorem ContinuousMap.isClopen_setOf_mapsTo

added theorem ContinuousMap.isClosed_setOf_mapsTo

Modified Mathlib/Topology/Constructions.lean

added theorem IsClosed.setOf_mapsTo

Modified Mathlib/Topology/Sets/Closeds.lean

added theorem TopologicalSpace.Clopens.mem_mk

Modified docs/references.bib