iUnion_openCell_eq_skeletonLT — Mathlib

English

For RelCWComplex C D, the union over openCell m j for m < n is contained in skeletonLT C n.

Русский

Для RelCWComplex C D объединение openCell m j по m < n содержится в skeletonLT C n.

LaTeX

$$$\\bigcup_{m< n} \\bigcup_{j\\in\\mathrm{cell}(C,m)} \\mathrm{openCell}(m,j) \\subseteq \\mathrm{skeletonLT}(C,D;n)$$$

Lean4

/-- A version of the definition of `skeletonLT` with open cells. -/
theorem iUnion_openCell_eq_skeletonLT [RelCWComplex C D] (n : ℕ∞) :
    D ∪ ⋃ (m : ℕ) (_ : m < n) (j : cell C m), openCell m j = skeletonLT C n :=
  (coe_skeletonLT C _).symm ▸ RelCWComplex.iUnion_openCell_eq_iUnion_closedCell n

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