instNontrivialSubobjectOfSimple

Mathlib.CategoryTheory.Simple

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instNontrivialSubobjectOfSimple

English

For a simple object X, Subobject X is nontrivial.

Русский

Для простого X подобъект X ненулевой.

LaTeX

$$$ \text{Nontrivial}(\mathrm{Subobject}(X)). $$$

Lean4

instance {X : C} [Simple X] : Nontrivial (Subobject X) :=
  nontrivial_of_not_isZero (Simple.not_isZero X)

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

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

Разделы

Аффилиация

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