map₂_fst — Mathlib

English

The yonedaEquivFst component after map₂ corresponds to A.map f.op applied to p.yonedaEquivFst.

Русский

После map₂ компонент yonedaEquivFst соответствует A.map f.op применённому к p.yonedaEquivFst.

LaTeX

$$$\\forall {Y} (f : X \\to Y) (p : YonedaCollection F Y), (YonedaCollection.map₂ F f p).yonedaEquivFst = A.map f.op \\; p.yonedaEquivFst$$$

Lean4

@[simp]
theorem map₂_fst {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).fst = yoneda.map f ≫ p.fst := by simp [map₂]

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