monotone_chain_condition_of_isNoetherianObject

English

If X is Noetherian, then for any f : Nat → Subobject(X) that is monotone, there exists n such that for all m ≥ n we have f(n) = f(m).

Русский

Если X — нётеровский, то любая монотонная цепь подобъектов X стабилизируется: существует n, такое что для всех m ≥ n выполняется f(n) = f(m).

LaTeX

$$$[\text{IsNoetherianObject}(X)] \Rightarrow \forall f: \mathrm{OrderHom}(\mathbb{N}, \mathrm{Subobject}(X)),\ \exists n\,\forall m\, (n \le m) \rightarrow f(n)=f(m).$$$

Lean4

theorem monotone_chain_condition_of_isNoetherianObject [IsNoetherianObject X] (f : ℕ →o Subobject X) :
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m :=
  (isNoetherianObject_iff_monotone_chain_condition X).1 inferInstance f

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