isEventuallyConstant_of_isArtinianObject

English

If X is Artinian, then any F: Nat ⥤ (MonoOver X)ᵒᵖ is eventually constant.

Русский

Если X артинян, то любая F: Nat ⥤ (MonoOver X)ᵒᵖ становится константной на некотором конечном шаге.

LaTeX

$$$[IsArtinianObject X] (F : \\mathbb{N} \\to (\\mathrm{MonoOver}(X))^{\\mathrm{op}}) : \\mathrm{IsFiltered.IsEventuallyConstant} F$$$

Lean4

theorem isEventuallyConstant_of_isArtinianObject [IsArtinianObject X] (F : ℕ ⥤ (MonoOver X)ᵒᵖ) :
    IsFiltered.IsEventuallyConstant F :=
  (isArtinianObject_iff_isEventuallyConstant X).1 inferInstance F

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