pullbackIsoPullback_hom_snd — Mathlib

English

Similarly, the snd component of pullback_hom_fst matches the explicit pullback snd.

Русский

Аналогично, вторая компонента pullback_hom_fst совпадает с явной snd.

LaTeX

$$$((pullbackIsoPullback f g).hom p).\\mathrm{snd} = (pullback.snd f g) p$$$

Lean4

@[simp]
theorem pullbackIsoPullback_hom_snd (p : pullback f g) :
    ((pullbackIsoPullback f g).hom p : X × Y).snd = (pullback.snd f g) p :=
  PullbackCone.IsLimit.equivPullbackObj_apply_snd (pullbackIsPullback f g) p

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