equivPullbackObj_apply_fst — Mathlib

English

The first projection via the equivalence identifies with the explicit fst on the pullback.

Русский

Первая проекция через эквивалентность совпадает с явной fst на pullback.

LaTeX

$$$ (equivPullbackObj hc x).1.1 = c.fst x $$$

Lean4

@[simp]
theorem equivPullbackObj_apply_fst (x : c.pt) : (equivPullbackObj hc x).1.1 = c.fst x :=
  congr_fun (IsLimit.conePointUniqueUpToIso_hom_comp hc (Types.pullbackLimitCone f g).isLimit .left) x

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