skeleton — Mathlib

English

For a RelCWComplex C D, and n ∈ ℕ∞, the skeleton of C is defined by skeleton(C; n) = skeletonLT(C; n+1).

Русский

Для относительного CW-комплекса C D скелет(C; n) задаётся как skeletonLT(C; n+1).

LaTeX

$$$\\mathrm{skeleton}(C; n)=\\mathrm{skeletonLT}(C; n+1) \\quad(n\\in\\mathbb{N}\\cup\\{\\infty\\})$$$

Lean4

/-- The `n`-skeleton of a CW complex, for `n ∈ ℕ ∪ {∞}`. For statements use `skeletonLT` instead
and then derive the statement about `skeleton`. -/
abbrev skeleton (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Subcomplex C :=
  skeletonLT C (n + 1)

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