of_is_product' — Mathlib

English

If there is a limit for BinaryFan.mk fst snd and a terminal object, then the maps to terminal yield IsPullback.

Русский

Если существует предел BinaryFan.mk fst snd и терминальный объект, то карты в терминал образуют IsPullback.

LaTeX

$$IsPullback fst snd (terminal.from X) (terminal.from Y)$$

Lean4

/-- A variant of `of_is_product` that is more useful with `apply`. -/
theorem of_is_product' (h : Limits.IsLimit (BinaryFan.mk fst snd)) (t : IsTerminal Z) :
    IsPullback fst snd (t.from _) (t.from _) :=
  of_is_product h t

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