equivPullbackObj_apply_snd — Mathlib

English

Similarly, the second projection corresponds to the explicit snd on the pullback under the equivalence.

Русский

Аналогично, вторая проекция соответствует явной snd через эквив.

LaTeX

$$$ (equivPullbackObj hc x).1.2 = c.snd x $$$

Lean4

@[simp]
theorem equivPullbackObj_apply_snd (x : c.pt) : (equivPullbackObj hc x).1.2 = c.snd x :=
  congr_fun (IsLimit.conePointUniqueUpToIso_hom_comp hc (Types.pullbackLimitCone f g).isLimit .right) x

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