yonedaEquiv_coe — Mathlib

English

The value of the coefficient of yonedaEquiv at f matches yonedaEquiv of the composite f ≫ A.ι.

Русский

Значение коэффициента yonedaEquiv на f равно yonedaEquiv( f ≫ A.ι ).

LaTeX

$$(DFunLike.coe (F := ((stdSimplex.obj n ⟶ Subpresheaf.toPresheaf A) ≃ A.obj (op n))) yonedaEquiv f).val = yonedaEquiv (f ≫ A.ι)$$

Lean4

theorem yonedaEquiv_coe {A : X.Subcomplex} {n : SimplexCategory} (f : stdSimplex.obj n ⟶ A) :
    (DFunLike.coe (F := ((stdSimplex.obj n ⟶ Subpresheaf.toPresheaf A) ≃ A.obj (op n))) yonedaEquiv f).val =
      yonedaEquiv (f ≫ A.ι) :=
  by rfl

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