English
Let (C, D) be a RelCWComplex. For n ≤ m, the intersection of skeletonLT(C, n) with a closed cell equals its intersection with the cell frontier: skeletonLT(C, n) ∩ closedCell(m, j) = skeletonLT(C, n) ∩ cellFrontier(m, j).
Русский
Пусть (C, D) — RelCWComplex. При n ≤ m пересечение skeletonLT(C, n) с закрытой клеткой совпадает с пересечением с границей клетки: skeletonLT(C, n) ∩ closedCell(m, j) = skeletonLT(C, n) ∩ cellFrontier(m, j).
LaTeX
$$$$ (skeletonLT\\,C\\,n) \\cap \\text{closedCell}(m,j) = (skeletonLT\\,C\\,n) \\cap \\text{cellFrontier}(m,j) $$$$
Lean4
/-- A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with
the boundary of the cell. -/
theorem skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m}
(hnm : n ≤ m) : (skeletonLT C n : Set X) ∩ closedCell m j = (skeletonLT C n : Set X) ∩ cellFrontier m j :=
by
refine subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_closedCell _ _))
rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
apply union_subset (by rfl)
rw [(disjoint_skeletonLT_openCell hnm).inter_eq]
exact empty_subset _
