δ_obj — Mathlib

English

In the nerve of a category, the δ-face object at i and j corresponds to the component at succAbove.

Русский

У δ-ответа нерва категории соответствующая компонентная часть соответствует succAbove.

LaTeX

$$$ ((\nerve C).δ i x).obj j = x.obj (i.succAbove j) $$$

Lean4

theorem δ_obj {n : ℕ} (i : Fin (n + 2)) (x : (nerve C) _⦋n + 1⦌) (j : Fin (n + 1)) :
    ((nerve C).δ i x).obj j = x.obj (i.succAbove j) :=
  rfl

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