of_hasBinaryProduct' — Mathlib

English

If X,Y have binary products and a terminal object exists, then the canonical pullback of terminal projections is an IsPullback.

Русский

Если у X,Y есть двоичное произведение и существует терминальный объект, то канонический пуллбек проекций в терминал является IsPullback.

LaTeX

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

Lean4

theorem of_hasBinaryProduct' [HasBinaryProduct X Y] [HasTerminal C] :
    IsPullback Limits.prod.fst Limits.prod.snd (terminal.from X) (terminal.from Y) :=
  of_is_product (limit.isLimit _) terminalIsTerminal

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