Commit 2026-06-13 14:25 e0cf79c4

View on Github →

feat: use alias_in attribute for CW complexes (#38785) Using the alias_in attribute for classical CW complexes to get rid of the export sections.

Estimated changes

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

deleted theorem Topology.CWComplex.CWComplex.exists_mem_openCell_of_mem_skeleton

deleted theorem Topology.CWComplex.CWComplex.iUnion_openCell_eq_skeleton

deleted theorem Topology.CWComplex.CWComplex.iUnion_openCell_eq_skeletonLT

deleted theorem Topology.CWComplex.CWComplex.mem_skeletonLT_iff

deleted theorem Topology.CWComplex.CWComplex.skeletonLT_zero_eq_empty

deleted theorem Topology.CWComplex.RelCWComplex.cellFrontier_subset_skeleton

deleted theorem Topology.CWComplex.RelCWComplex.cellFrontier_subset_skeletonLT

deleted theorem Topology.CWComplex.RelCWComplex.closedCell_subset_skeleton

deleted theorem Topology.CWComplex.RelCWComplex.closedCell_subset_skeletonLT

deleted theorem Topology.CWComplex.RelCWComplex.disjoint_interior_base_closedCell

deleted theorem Topology.CWComplex.RelCWComplex.disjoint_interior_base_iUnion_closedCell

deleted theorem Topology.CWComplex.RelCWComplex.disjoint_skeletonLT_openCell

deleted theorem Topology.CWComplex.RelCWComplex.disjoint_skeleton_openCell

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_cellFrontier_subset_skeleton

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_openCell_eq_skeleton

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_openCell_eq_skeletonLT

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_skeletonLT_eq_complex

deleted theorem Topology.CWComplex.RelCWComplex.iUnion_skeleton_eq_complex

deleted theorem Topology.CWComplex.RelCWComplex.mem_skeletonLT_iff

deleted theorem Topology.CWComplex.RelCWComplex.mem_skeleton_iff

deleted theorem Topology.CWComplex.RelCWComplex.openCell_subset_skeleton

deleted theorem Topology.CWComplex.RelCWComplex.openCell_subset_skeletonLT

deleted def Topology.CWComplex.RelCWComplex.skeletonLT

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_mono

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_monotone

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_top

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

deleted theorem Topology.CWComplex.RelCWComplex.skeletonLT_zero_eq_base

deleted theorem Topology.CWComplex.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

deleted theorem Topology.CWComplex.RelCWComplex.skeleton_mono

deleted theorem Topology.CWComplex.RelCWComplex.skeleton_monotone

deleted theorem Topology.CWComplex.RelCWComplex.skeleton_top

deleted theorem Topology.CWComplex.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ

deleted def Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.mk''

deleted def Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.mk'

deleted theorem Topology.CWComplex.Subcomplex.CWComplex.Subcomplex.union

deleted theorem Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.base_subset

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

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

deleted theorem Topology.CWComplex.Subcomplex.RelCWComplex.Subcomplex.subset_complex

added def Topology.CWComplex.Subcomplex.mk''

added def Topology.CWComplex.Subcomplex.mk'

added theorem Topology.CWComplex.Subcomplex.union

added theorem Topology.CWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.CWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.CWComplex.mem_skeletonLT_iff

added theorem Topology.CWComplex.mem_skeleton_iff

added theorem Topology.CWComplex.skeletonLT_zero_eq_empty

added theorem Topology.RelCWComplex.Subcomplex.base_subset

modified theorem Topology.RelCWComplex.Subcomplex.coe_copy

modified theorem Topology.RelCWComplex.Subcomplex.ext

added def Topology.RelCWComplex.Subcomplex.mk''

added def Topology.RelCWComplex.Subcomplex.mk'

added theorem Topology.RelCWComplex.Subcomplex.subset_complex

added theorem Topology.RelCWComplex.cellFrontier_subset_skeleton

added theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT

added theorem Topology.RelCWComplex.closedCell_subset_skeleton

added theorem Topology.RelCWComplex.closedCell_subset_skeletonLT

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.iUnion_cellFrontier_subset_skeleton

added theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT

added theorem Topology.RelCWComplex.iUnion_openCell_eq_skeleton

added theorem Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT

added theorem Topology.RelCWComplex.iUnion_skeletonLT_eq_complex

added theorem Topology.RelCWComplex.iUnion_skeleton_eq_complex

added theorem Topology.RelCWComplex.mem_skeletonLT_iff

added theorem Topology.RelCWComplex.mem_skeleton_iff

added theorem Topology.RelCWComplex.openCell_subset_skeleton

added theorem Topology.RelCWComplex.openCell_subset_skeletonLT

added def Topology.RelCWComplex.skeletonLT

added theorem Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier

added theorem Topology.RelCWComplex.skeletonLT_mono

added theorem Topology.RelCWComplex.skeletonLT_monotone

added theorem Topology.RelCWComplex.skeletonLT_top

added theorem Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

added theorem Topology.RelCWComplex.skeletonLT_zero_eq_base

added theorem Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier

added theorem Topology.RelCWComplex.skeleton_mono

added theorem Topology.RelCWComplex.skeleton_monotone

added theorem Topology.RelCWComplex.skeleton_top

added theorem Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ

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

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