isoNerve_inv_app_apply — Mathlib

English

The i-th component of the inverse of the nerve isomorphism applied to F is F.obj i's downward component.

Русский

i-й компонент обратного нерва-изоморфизма, применённого к F, равен downward-коэффициенту F (i).

LaTeX

$$(isoNerve.{u} n).inv.app _ F i = (F.obj i).down$$

Lean4

@[simp]
theorem isoNerve_inv_app_apply {n d : ℕ} (F : (nerve (ULift.{u} (Fin (n + 1)))) _⦋d⦌) (i : Fin (d + 1)) :
    (isoNerve.{u} n).inv.app _ F i = (F.obj i).down :=
  rfl

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