pullbackIsoPullback_inv_snd_apply

English

Similarly, applying the inverse pullbackIsoPullback to x and then snd yields the second coordinate of x.

Русский

Аналогично: применяя обратный pullbackIsoPullback к x и затем snd, получаем вторую координату x.

LaTeX

$$$\\forall x,\\; (pullback.snd\\, f\\, g)\\big((pullbackIsoPullback\\ f\\ g)^{-1} x\\big) = \\big(\\lambda p. p.2\\colon X\\times Y\\to Y\\big) x.$$$

Lean4

@[simp]
theorem pullbackIsoPullback_inv_snd_apply (x : (Types.pullbackCone f g).pt) :
    (pullback.snd f g) ((pullbackIsoPullback f g).inv x) = (fun p => (p.1 : X × Y).snd) x :=
  PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd (pullbackIsPullback f g) x

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