Commit 2025-09-17 11:12 9a09b748

View on Github →

feat: a subcomplex of a classical CW complex is a CW complex (#29177) This PR proves that any subcomplex of a (relative classical) CW complex is again a CW complex.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

added theorem Topology.CWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell

added theorem Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell

Created Mathlib/Topology/CWComplex/Classical/Subcomplex.lean

added theorem Topology.CWComplex.Subcomplex.cell_def

added theorem Topology.CWComplex.Subcomplex.map_def

added theorem Topology.CWComplex.Subcomplex.union_closedCell

added theorem Topology.RelCWComplex.Subcomplex.cellFrontier_eq

added theorem Topology.RelCWComplex.Subcomplex.cellFrontier_subset_of_mem

added theorem Topology.RelCWComplex.Subcomplex.closedCell_eq

added theorem Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem

added theorem Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem

added theorem Topology.RelCWComplex.Subcomplex.openCell_eq

added theorem Topology.RelCWComplex.Subcomplex.openCell_subset_of_mem

added theorem Topology.RelCWComplex.Subcomplex.union_closedCell

Modified docs/references.bib