wellFoundedGT — Mathlib

English

If M is Noetherian, then the strict greater-than relation on submodules of M is well-founded; equivalently, there are no infinite descending chains of submodules under inclusion.

Русский

Если M — нётеров модуль, то строгое отношение «больше» между подмодулями M является хорошо основанным; то есть бесконечных нисходящих цепей подмодулей по включению нет.

LaTeX

$$$\\text{IsNoetherian}(R,M) \\Rightarrow \\operatorname{WellFounded}((>): \\text{Submodule}_R(M) \\to \\text{Submodule}_R(M) \\to \\operatorname{Prop})$$$

Lean4

instance wellFoundedGT [h : IsNoetherian R M] : WellFoundedGT (Submodule R M) :=
  h.wellFoundedGT

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