hasLimit_pair — Mathlib

English

If there is a binary biproduct for P and Q, then the limit of the pair diagram (pair P Q) exists.

Русский

Если существует бинарное би-произведение для объектов P и Q, то предел диаграммы пары (pair P Q) существует.

LaTeX

$$$ HasBinaryBiproduct P Q \Rightarrow HasLimit (\text{pair } P Q). $$$

Lean4

instance hasLimit_pair [HasBinaryBiproduct P Q] : HasLimit (pair P Q) :=
  HasLimit.mk ⟨_, BinaryBiproduct.isLimit P Q⟩

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