instSimpleSimpleSubobject — Mathlib

English

If X is Artinian, then for any Not-IsZero X with HasZeroMorphisms and HasZeroObject, there exists a simple subobject of X.

Русский

Если X артинян, тогда для любого не нулевого X с нулепорождающими морфизмами и нулевым объектом существует простой подобъект X.

LaTeX

$$$[IsArtinianObject X] \\Rightarrow \\forall h: \\mathrm{not}\\;IsZero(X) \\Rightarrow \\mathrm{Simple}(\\mathrm{simpleSubobject}\,h)$$$

Lean4

instance {X : C} [IsArtinianObject X] (h : ¬IsZero X) : Simple (simpleSubobject h) :=
  (exists_simple_subobject h).choose_spec

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