skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ

English

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

Русский

Для RelCWComplex C D скелет LT(n) объединение с ⋃ замкнутые клетки при n даёт skeletonLT(n+1).

LaTeX

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

Lean4

theorem skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ [RelCWComplex C D] (n : ℕ) :
    (skeletonLT C n : Set X) ∪ ⋃ (j : cell C n), closedCell n j = skeletonLT C (n + 1) :=
  by
  rw [coe_skeletonLT, coe_skeletonLT, union_assoc]
  congr
  norm_cast
  exact (biUnion_lt_succ _ _).symm

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