isEventuallyConstant_of_isNoetherianObject

English

If X is Noetherian, any diagram F: Nat ⥤ MonoOver X becomes constant after some index.

Русский

Если X нётеровский, любая диаграмма F: Nat ⥤ MonoOver X становится константной после некоторого индекса.

LaTeX

$$$[\text{IsNoetherianObject}(X)] \Rightarrow \forall F:\mathbb{N} \to \mathrm{MonoOver}(X),\ \mathrm{IsFiltered.IsEventuallyConstant}(F).$$$

Lean4

theorem isEventuallyConstant_of_isNoetherianObject [IsNoetherianObject X] (F : ℕ ⥤ MonoOver X) :
    IsFiltered.IsEventuallyConstant F :=
  (isNoetherianObject_iff_isEventuallyConstant X).1 inferInstance F

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