ι — Mathlib · SciLib

English

For a cell γ in a relative cell complex, i is the index in the family of basic morphisms corresponding to γ, i = i(γ).

Русский

Для клетки γ в относительном клеточном комплексе i — индекс семейства базовых морфизмов, соответствующий γ.

LaTeX

$$$i(\gamma) : α_{\gamma.j}$$$

Lean4

/-- The inclusion of a cell. -/
def ι (γ : Cells c) : B γ.j γ.i ⟶ Y :=
  (c.attachCells γ.j γ.hj).cell γ.k ≫ c.incl.app (Order.succ γ.j)

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