Commit 2025-08-29 09:05 59d5f66b

View on Github →

feat: subcomplexes of a classical CW complex (#26201) This PR defines subcomplexes of a (classical relative) CW complex to be a closed subspace which is a union of open cells. It provides additional definitions for alternative ways to describe subcomplexes. Lastly, it refactors the definition of the skeleton to define it as a subcomplex.

Estimated changes

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

added theorem Topology.CWComplex.CWComplex.exists_mem_openCell_of_mem_skeleton

added theorem Topology.CWComplex.CWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.CWComplex.CWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.CWComplex.CWComplex.mem_skeletonLT_iff

added theorem Topology.CWComplex.CWComplex.skeletonLT_zero_eq_empty

added theorem Topology.CWComplex.RelCWComplex.cellFrontier_subset_skeleton

added theorem Topology.CWComplex.RelCWComplex.cellFrontier_subset_skeletonLT

added theorem Topology.CWComplex.RelCWComplex.closedCell_subset_skeleton

added theorem Topology.CWComplex.RelCWComplex.closedCell_subset_skeletonLT

added theorem Topology.CWComplex.RelCWComplex.disjoint_interior_base_closedCell

added theorem Topology.CWComplex.RelCWComplex.disjoint_interior_base_iUnion_closedCell

added theorem Topology.CWComplex.RelCWComplex.disjoint_skeletonLT_openCell

added theorem Topology.CWComplex.RelCWComplex.disjoint_skeleton_openCell

added theorem Topology.CWComplex.RelCWComplex.iUnion_cellFrontier_subset_skeleton

added theorem Topology.CWComplex.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT

added theorem Topology.CWComplex.RelCWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.CWComplex.RelCWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.CWComplex.RelCWComplex.iUnion_skeletonLT_eq_complex

added theorem Topology.CWComplex.RelCWComplex.iUnion_skeleton_eq_complex

added theorem Topology.CWComplex.RelCWComplex.mem_skeletonLT_iff

added theorem Topology.CWComplex.RelCWComplex.mem_skeleton_iff

added theorem Topology.CWComplex.RelCWComplex.openCell_subset_skeleton

added theorem Topology.CWComplex.RelCWComplex.openCell_subset_skeletonLT

added def Topology.CWComplex.RelCWComplex.skeletonLT

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_mono

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_monotone

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_top

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

added theorem Topology.CWComplex.RelCWComplex.skeletonLT_zero_eq_base

added theorem Topology.CWComplex.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

added theorem Topology.CWComplex.RelCWComplex.skeleton_mono

added theorem Topology.CWComplex.RelCWComplex.skeleton_monotone

added theorem Topology.CWComplex.RelCWComplex.skeleton_top

added theorem Topology.CWComplex.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ

added def Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.mk''

added def Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.mk'

added theorem Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.union

added theorem Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.base_subset

added def Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.mk''

added def Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.mk'

added theorem Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.subset_complex

deleted theorem Topology.CWComplex.exists_mem_openCell_of_mem_skeleton

deleted theorem Topology.CWComplex.iUnion_openCell_eq_skeleton

deleted theorem Topology.CWComplex.iUnion_openCell_eq_skeletonLT

deleted theorem Topology.CWComplex.mem_skeletonLT_iff

deleted theorem Topology.CWComplex.skeletonLT_zero_eq_empty

added theorem Topology.RelCWComplex.Subcomplex.closed

added theorem Topology.RelCWComplex.Subcomplex.coe_copy

added theorem Topology.RelCWComplex.Subcomplex.coe_eq_carrier

added theorem Topology.RelCWComplex.Subcomplex.copy_eq

added theorem Topology.RelCWComplex.Subcomplex.eq_iff

added theorem Topology.RelCWComplex.Subcomplex.ext

added theorem Topology.RelCWComplex.Subcomplex.mem_carrier

added theorem Topology.RelCWComplex.Subcomplex.union

added structure Topology.RelCWComplex.Subcomplex

deleted theorem Topology.RelCWComplex.base_subset_skeleton

deleted theorem Topology.RelCWComplex.base_subset_skeletonLT

deleted theorem Topology.RelCWComplex.cellFrontier_subset_skeleton

deleted theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT

deleted theorem Topology.RelCWComplex.closedCell_subset_skeleton

deleted theorem Topology.RelCWComplex.closedCell_subset_skeletonLT

deleted theorem Topology.RelCWComplex.disjoint_interior_base_closedCell

deleted theorem Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell

deleted theorem Topology.RelCWComplex.disjoint_skeletonLT_openCell

deleted theorem Topology.RelCWComplex.disjoint_skeleton_openCell

deleted theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton

deleted theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT

deleted theorem Topology.RelCWComplex.iUnion_openCell_eq_skeleton

deleted theorem Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT

deleted theorem Topology.RelCWComplex.iUnion_skeletonLT_eq_complex

deleted theorem Topology.RelCWComplex.iUnion_skeleton_eq_complex

deleted theorem Topology.RelCWComplex.mem_skeletonLT_iff

deleted theorem Topology.RelCWComplex.mem_skeleton_iff

deleted theorem Topology.RelCWComplex.openCell_subset_skeleton

deleted theorem Topology.RelCWComplex.openCell_subset_skeletonLT

deleted def Topology.RelCWComplex.skeleton

deleted def Topology.RelCWComplex.skeletonLT

deleted theorem Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier

deleted theorem Topology.RelCWComplex.skeletonLT_mono

deleted theorem Topology.RelCWComplex.skeletonLT_monotone

deleted theorem Topology.RelCWComplex.skeletonLT_subset_complex

deleted theorem Topology.RelCWComplex.skeletonLT_top

deleted theorem Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

deleted theorem Topology.RelCWComplex.skeletonLT_zero_eq_base

deleted theorem Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

deleted theorem Topology.RelCWComplex.skeleton_mono

deleted theorem Topology.RelCWComplex.skeleton_monotone

deleted theorem Topology.RelCWComplex.skeleton_subset_complex

deleted theorem Topology.RelCWComplex.skeleton_top

deleted theorem Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ