subsingleton_of_isZero

Mathlib.CategoryTheory.Subobject.Lattice

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.subsingleton_of_isZero

English

If X is a zero object, Subobject X is subsingleton.

Русский

Если X нулевой объект, то Subobject X — это подпорядок-одиночный.

LaTeX

$$IsZero X → Subsingleton (Subobject X)$$

Lean4

theorem subsingleton_of_isZero {X : C} (hX : IsZero X) : Subsingleton (Subobject X) :=
  subsingleton_of_isInitial hX.isInitial

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

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

Разделы

Аффилиация

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