pullbackIsoPullback_inv_fst_apply

English

For a pullback square with f: X→Z and g: Y→Z, applying the inverse of the pullbackIsoPullback to x and then fst yields the first coordinate of x.

Русский

В квадрате pullback с f: X→Z и g: Y→Z, применение обратного изоморфизма pullbackIsoPullback к x и далее fst дает первую координату x.

LaTeX

$$$\\forall x \\in (\\text{Types.pullbackCone } f g).pt,\\; (pullback.fst\\, f\\, g)\\big((pullbackIsoPullback\\ f\\ g)^{-1} x\\big) = \\big(\\lambda p. p.1\\colon X\\times Y\\to X\\big) x.$$$

Lean4

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

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