toKaroubiCompN₂IsoN₁_inv_app — Mathlib

English

The inverse side of the canonical isomorphism applied to a simplicial object X has its f-component equal to PInfty when evaluated at the appropriate level.

Русский

Обратная часть канонического изоморфизма, применённого к симплициальному объекту X, имеет компонент f равный PInfty на соответствующем уровне.

LaTeX

$$$\big( toKaroubiCompN₂IsoN₁^{-1} \big)_{\mathrm{app}}(X).f = PInfty$$$

Lean4

@[simp]
theorem toKaroubiCompN₂IsoN₁_inv_app (X : SimplicialObject C) : (toKaroubiCompN₂IsoN₁.inv.app X).f = PInfty :=
  rfl

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