yonedaEquiv_comp — Mathlib

English

For morphisms f: stdSimplex.obj n ⟶ X and g: X ⟶ Y, the Yoneda equivalence is compatible with composition: yonedaEquiv (f ≫ g) = g.app _ (yonedaEquiv f).

Русский

Для морфизмов f и g Композиция сохраняет соответствие Яниды: yonedaEquiv(f ≫ g) = g.app _ (yonedaEquiv f).

LaTeX

$$yonedaEquiv (f ≫ g) = g.app _ (yonedaEquiv f)$$

Lean4

theorem yonedaEquiv_comp {X Y : SSet.{u}} {n : SimplexCategory} (f : stdSimplex.obj n ⟶ X) (g : X ⟶ Y) :
    yonedaEquiv (f ≫ g) = g.app _ (yonedaEquiv f) :=
  rfl

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