map₂_snd — Mathlib

English

The snd-component after map₂ equals the image under F of p.snd after precomposing with CostructuredArrow.mkPrecomp.

Русский

После map₂ вторая компонента равна сохранению через F от p.snd после предкомпозиции с CostructuredArrow.mkPrecomp.

LaTeX

$$$\\forall {Y} (f : X ⟶ Y) (p : YonedaCollection F Y), \\\\ (YonedaCollection.map₂ F f p).snd = \\\\ F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom (by rw [YonedaCollection.map₂_fst f])) p.snd$$$

Lean4

@[simp]
theorem map₂_snd {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).snd =
      F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom (by rw [YonedaCollection.map₂_fst f])) p.snd :=
  by simp [map₂]

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