skeleton_union_iUnion_closedCell_eq_skeleton_succ

English

For RelCWComplex C D, skeletonLT(C; n) ∪ ⋃_{j∈cell C(n+1)} closedCell(n+1) j equals skeleton(C; n+1).

Русский

Для RelCWComplex C D, skeletonLT(n) ∪ ⋃ замкнутых клеток n+1 равняется skeleton(n+1).

LaTeX

$$$\\mathrm{skeletonLT}(C,D;n) \\cup \\bigcup_{j\\in\\mathrm{cell}(C,n+1)}\\mathrm{closedCell}(n+1,j)=\\mathrm{skeleton}(C,D;n+1)$$$

Lean4

theorem skeleton_union_iUnion_closedCell_eq_skeleton_succ [RelCWComplex C D] (n : ℕ) :
    (skeleton C n : Set X) ∪ ⋃ (j : cell C (n + 1)), closedCell (n + 1) j = skeleton C (n + 1) :=
  skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ _

Похожие утверждения