hasBinaryProduct_zero_right

Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasBinaryProduct_zero_right

English

For any object X, the binary product X × 0 exists.

Русский

Для любого объекта X существует двоичное произведение X × 0.

LaTeX

$$$$\text{HasBinaryProduct } X\; 0.$$$

Lean4

instance hasBinaryProduct_zero_right (X : C) : HasBinaryProduct X (0 : C) :=
  HasLimit.mk ⟨_, binaryFanZeroRightIsLimit X⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru