opFunctor_obj_δ — Mathlib

English

For i : Fin(n+2) and x : Fin(n+3), map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x.

Русский

Для i : Fin(n+2) и x : Fin(n+3) выполняется map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x.

LaTeX

$$$map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x$$$

Lean4

@[simp]
theorem opFunctor_obj_δ (X : SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) :
    (opFunctor.obj X).δ i = opObjIso.hom ≫ X.δ i.rev ≫ opObjIso.inv := by simp [SimplicialObject.δ]

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