not_strictAnti_of_isArtinianObject

English

If X is Artinian, then any given sequence of subobjects cannot be strictly anti.

Русский

Если X артинян, то любая последовательность подобъектов не может быть строго антицепью.

LaTeX

$$$[IsArtinianObject X] \\Rightarrow \\forall f: \\mathbb{N} \\to \\mathrm{Subobject}(X), \\neg \\mathrm{StrictAnti}(f)$$$

Lean4

theorem not_strictAnti_of_isArtinianObject [IsArtinianObject X] (f : ℕ → Subobject X) : ¬StrictAnti f :=
  (isArtinianObject_iff_not_strictAnti X).1 inferInstance f

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