eventuallyConst_of_isArtinian — Mathlib

English

If M is Artinian, then every order-preserving map f from Nat to Submodule R M is eventually constant atTop.

Русский

Если M артинанов, то любая монотонная карта f: Nat → Submodule R M становится постоянной на бесконечной части, т.е. на верхнем пределе.

LaTeX

$$$\\text{IsArtinian}\\ R\\ M \\Rightarrow atTop.EventuallyConst\\ f$$$

Lean4

theorem eventuallyConst_of_isArtinian (f : ℕ →o (Submodule R M)ᵒᵈ) : atTop.EventuallyConst f :=
  by
  simp_rw [eventuallyConst_atTop, eq_comm]
  exact monotone_stabilizes f

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