wellFoundedLT_of_isArtinian — Mathlib

English

If M is Artinian, then the strict order LT on Lie submodules is well-founded; ascending chains stabilize.

Русский

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

LaTeX

$$IsArtinian R M \\Rightarrow WellFoundedLT (LieSubmodule R L M)$$

Lean4

theorem wellFoundedLT_of_isArtinian [IsArtinian R M] : WellFoundedLT (LieSubmodule R L M) :=
  RelHomClass.isWellFounded (toSubmodule_orderEmbedding R L M).ltEmbedding

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