eventuallyConst_of_isNoetherian — Mathlib

English

If M is a Noetherian R-module, then every monotone order-preserving map f from natural numbers to submodules of M is eventually constant.

Русский

Если M — Нётеров R-модуль, то любая монотонная отображение из натуральных чисел в подмодули M стабилизируется.

LaTeX

$$$[\\text{IsNoetherian }R\\ M] \\Rightarrow \\forall f: \\mathbb{N} \\to_o \\mathrm{Submodule}_R(M),\\ atTop\\text{.EventualConst } f$$$

Lean4

theorem eventuallyConst_of_isNoetherian [IsNoetherian R M] (f : ℕ →o Submodule R M) : atTop.EventuallyConst f :=
  by
  simp_rw [eventuallyConst_atTop, eq_comm]
  exact (monotone_stabilizes_iff_noetherian.mpr inferInstance) f

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