iUnion_openCell_eq_skeleton — Mathlib

English

Equivalence relating iUnion of open cells and skeletonLT via a canonical translation.

Русский

Эквивалентность, связывающая iUnion открытых клеток и skeletonLT через каноническое отображение.

LaTeX

$$$\\text{(iUnion openCell)}\\;=\\;\\mathrm{skeletonLT}(C,D; n)$$$

Lean4

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

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