Commit 2025-03-05 17:02 daac3d17

View on Github →

feat: additional basic lemmas about CW complexes (#20287) This PR adds additional basic lemmas about the classical definition of CW complexes.

Estimated changes

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

added theorem Topology.CWComplex.cellFrontier_subset_finite_openCell

added theorem Topology.CWComplex.exists_mem_openCell_of_mem_skeleton

added theorem Topology.CWComplex.iUnion_openCell_eq_complex

added theorem Topology.CWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.CWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell

added theorem Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell

added theorem Topology.CWComplex.mem_skeletonLT_iff

added theorem Topology.RelCWComplex.cellFrontier_subset_complex

added theorem Topology.RelCWComplex.cellFrontier_subset_finite_openCell

added theorem Topology.RelCWComplex.disjoint_base_iUnion_openCell

added theorem Topology.RelCWComplex.disjoint_interior_base_closedCell

added theorem Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell

added theorem Topology.RelCWComplex.disjoint_skeletonLT_openCell

added theorem Topology.RelCWComplex.disjoint_skeleton_openCell

added theorem Topology.RelCWComplex.eq_of_not_disjoint_openCell

added theorem Topology.RelCWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.RelCWComplex.isClosed

added theorem Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell

added theorem Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell

added theorem Topology.RelCWComplex.mem_skeletonLT_iff

added theorem Topology.RelCWComplex.mem_skeleton_iff

added theorem Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier

added theorem Topology.RelCWComplex.skeletonLT_monotone

added theorem Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

added theorem Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

added theorem Topology.RelCWComplex.skeleton_monotone

added theorem Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ

added theorem Topology.RelCWComplex.union_iUnion_openCell_eq_complex