not_isZero

Mathlib.CategoryTheory.Simple

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Simple.not_isZero

English

A simple object X is not a zero object: IsZero(X) is false.

Русский

Простому объекту X не свойно быть нулём: IsZero(X) ложен.

LaTeX

$$$ \neg IsZero(X). $$$

Lean4

theorem not_isZero (X : C) [Simple X] : ¬IsZero X := by simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X

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

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

Разделы

Аффилиация

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