of_hasPullback — Mathlib

English

If HasPullback f g exists, then the canonical pullback is IsPullback.

Русский

Если существует HasPullback f g, то канонический пуллбек является IsPullback.

LaTeX

$$IsPullback (pullback.fst f g) (pullback.snd f g) f g$$

Lean4

/-- The pullback provided by `HasPullback f g` fits into an `IsPullback`. -/
theorem of_hasPullback (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    IsPullback (pullback.fst f g) (pullback.snd f g) f g :=
  of_isLimit (limit.isLimit (cospan f g))

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