wellFoundedGT_of_noetherian — Mathlib

English

If M is Noetherian as an R-module, then the reverse inclusion order on Lie submodules is well-founded; descending chains stabilize.

Русский

Если M является Noetherian относительно R-модуля, то обратная связка по включениям подмодулей Ли является хорошо основанной; нисходящие цепи стабилизируются.

LaTeX

$$IsNoetherian R M \\Rightarrow WellFoundedGT (LieSubmodule R L M)$$

Lean4

instance wellFoundedGT_of_noetherian [IsNoetherian R M] : WellFoundedGT (LieSubmodule R L M) :=
  RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).dual.ltEmbedding

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