wellFoundedGT_of_noetherian — Mathlib

English

If L is Noetherian as an R-Lie algebra, then the relation of Lie subalgebras under inclusion is well-founded with respect to the GT order; there are no infinite descending chains.

Русский

Если L является Noetherian как R-алгебра Ли, то отношение подалгебр по включению хорошо определено снизу, и не существует бесконечных нисходящих цепочек.

LaTeX

$$$ WellFoundedGT\\; (\\mathrm{LieSubalgebra}_R L) $$$

Lean4

instance wellFoundedGT_of_noetherian [IsNoetherian R L] : WellFoundedGT (LieSubalgebra R L) :=
  RelHomClass.isWellFounded (⟨toSubmodule, @fun _ _ h ↦ h⟩ : _ →r (· > ·))

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