hasZeroObject

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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

English

If X is zero, then C has a zero object.

Русский

Если X нулевой, то в C существует нулевой объект.

LaTeX

$$$\\\\forall X\\\\, IsZero(X) \\\\Rightarrow HasZeroObject(C)$$$

Lean4

theorem hasZeroObject {X : C} (hX : IsZero X) : HasZeroObject C :=
  ⟨⟨X, hX⟩⟩

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

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

Разделы

Аффилиация

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