iUnion_openCell_eq_skeleton — Mathlib

English

The union over all natural indices of skeletonLT equals the entire complex C.

Русский

Объединение по всем естественным индексам skeletonLT даёт весь комплекс C.

LaTeX

$$$\\bigcup_{n\\in\\mathbb{N}}\\mathrm{skeletonLT}(C,D;n)=C$$$

Lean4

theorem iUnion_openCell_eq_skeleton [CWComplex C] (n : ℕ∞) :
    ⋃ (m : ℕ) (_ : m < n + 1) (j : cell C m), openCell m j = skeleton C n :=
  iUnion_openCell_eq_skeletonLT _

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