monotone_stabilizes_iff_artinian — Mathlib

English

A module is Artinian iff every decreasing chain of submodules stabilizes.

Русский

Модуль артинанов тогда и только тогда, когда любая убывающая цепь подмодулей стабилизируется.

LaTeX

$$$(\\forall f: \\mathbb{N} \\to o(\\Submodule\\ R\\ M))\\, (\\exists n, \\forall m, n \\le m \\Rightarrow f(n) = f(m)) \\iff IsArtinian\\ R\\ M$$$

Lean4

/-- A module is Artinian iff every decreasing chain of submodules stabilizes. -/
theorem monotone_stabilizes_iff_artinian :
    (∀ f : ℕ →o (Submodule R M)ᵒᵈ, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsArtinian R M :=
  wellFoundedGT_iff_monotone_chain_condition.symm

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