i — Mathlib · SciLib

English

A relative cell complex c yields a transfinite composition of shape J of the coproducts of the family g, i.e., f is built as a transfinite sequence of pushouts of coproducts of g.

Русский

Относительный клеточный комплекс c задаёт трансфинитную композицию формы J из пушаутов копроподс семейства g в образе f.

LaTeX

$$$\\text{transfiniteCompositionOfShape} : \\text{(coproducts of ofHoms g)} \\to \\text{pushouts}^{J}(f)$$$

Lean4

/-- Given a cell `γ` in a relative cell complex, this is the corresponding
index in the family of morphisms `basicCell γ.j`. -/
def i (γ : Cells c) : α γ.j :=
  (c.attachCells γ.j γ.hj).π γ.k

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