feat: additional basic lemmas about CW complexes

[scholzhannah]

---

• depends on: feat : definition and basic lemmas about CW-complexes #19760

[mergify]

⚠️ The sha of the head commit of this PR conflicts with #19760. Mergify cannot evaluate rules on this PR. ⚠️

[github-actions]

PR summary 0b68c79e05

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.CWComplex.Basic (new file)	1721

---

Declarations diff

+ ClasCWComplex
+ ClasCWComplex.cellFrontier_subset_finite_closedCell
+ ClasCWComplex.cellFrontier_subset_finite_openCell
+ ClasCWComplex.closed
+ ClasCWComplex.exists_mem_openCell_of_mem_skeleton
+ ClasCWComplex.exists_mem_openCell_of_mem_skeletonLT
+ ClasCWComplex.iUnion_openCell
+ ClasCWComplex.iUnion_openCell_eq_skeleton
+ ClasCWComplex.iUnion_openCell_eq_skeletonLT
+ ClasCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell
+ ClasCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell
+ ClasCWComplex.mapsto
+ ClasCWComplex.mk.{u}
+ ClasCWComplex.skeletonLT_zero_eq_empty
+ ClasCWComplex.union
+ RelCWComplex.base_inter_iUnion_openCell_eq_empty
+ RelCWComplex.base_subset_complex
+ RelCWComplex.base_subset_skeleton
+ RelCWComplex.base_subset_skeletonLT
+ RelCWComplex.cellFrontier
+ RelCWComplex.cellFrontier_subset_base_union_finite_closedCell
+ RelCWComplex.cellFrontier_subset_closedCell
+ RelCWComplex.cellFrontier_subset_finite_openCell
+ RelCWComplex.cellFrontier_subset_skeleton
+ RelCWComplex.cellFrontier_subset_skeletonLT
+ RelCWComplex.cellFrontier_union_openCell_eq_closedCell
+ RelCWComplex.cellFrontier_zero_eq_empty
+ RelCWComplex.closed
+ RelCWComplex.closedCell
+ RelCWComplex.closedCell_subset_complex
+ RelCWComplex.closedCell_subset_skeleton
+ RelCWComplex.closedCell_subset_skeletonLT
+ RelCWComplex.closedCell_zero_eq_singleton
+ RelCWComplex.closure_openCell_eq_closedCell
+ RelCWComplex.disjointBase
+ RelCWComplex.disjoint_openCell_of_ne
+ RelCWComplex.eq_cell_of_not_disjoint
+ RelCWComplex.exists_mem_openCell_of_mem_skeleton
+ RelCWComplex.exists_mem_openCell_of_mem_skeletonLT
+ RelCWComplex.iUnion_cellFrontier_subset_skeleton
+ RelCWComplex.iUnion_cellFrontier_subset_skeletonLT
+ RelCWComplex.iUnion_openCell
+ RelCWComplex.iUnion_openCell_eq_skeleton
+ RelCWComplex.iUnion_openCell_eq_skeletonLT
+ RelCWComplex.iUnion_skeletonLT_eq_skeletonLT
+ RelCWComplex.iUnion_skeleton_eq_skeleton
+ RelCWComplex.interior_base_inter_closedCell_eq_empty
+ RelCWComplex.interior_base_inter_iUnion_closedCell_eq_empty
+ RelCWComplex.isClosed
+ RelCWComplex.isClosed_cellFrontier
+ RelCWComplex.isClosed_closedCell
+ RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell
+ RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell
+ RelCWComplex.isCompact_cellFrontier
+ RelCWComplex.isCompact_closedCell
+ RelCWComplex.map_zero_mem_closedCell
+ RelCWComplex.map_zero_mem_openCell
+ RelCWComplex.openCell
+ RelCWComplex.openCell_subset_closedCell
+ RelCWComplex.openCell_subset_complex
+ RelCWComplex.openCell_subset_skeleton
+ RelCWComplex.openCell_subset_skeletonLT
+ RelCWComplex.openCell_zero_eq_singleton
+ RelCWComplex.pairwiseDisjoint
+ RelCWComplex.skeleton
+ RelCWComplex.skeletonLT
+ RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier
+ RelCWComplex.skeletonLT_inter_openCell_eq_empty
+ RelCWComplex.skeletonLT_mono
+ RelCWComplex.skeletonLT_subset_complex
+ RelCWComplex.skeletonLT_succ_eq_skeletonLT_union_iUnion_closedCell
+ RelCWComplex.skeletonLT_top
+ RelCWComplex.skeletonLT_zero_eq_base
+ RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier
+ RelCWComplex.skeleton_inter_openCell_eq_empty
+ RelCWComplex.skeleton_mono
+ RelCWComplex.skeleton_subset_complex
+ RelCWComplex.skeleton_succ_eq_skeleton_union_iUnion
+ RelCWComplex.skeleton_top
+ RelCWComplex.union
+ RelCWComplex.{u}

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat : definition and basic lemmas about CW-complexes #19760
  By Dependent Issues (🤖). Happy coding!