isNoetherian_submodule_left — Mathlib

English

A module M over a semiring R is Noetherian if and only if the ordered set of its submodules is well-founded with respect to inclusion.

Русский

Модуль M над полем R Ноетерен тогда и только тогда, когда упорядоченный набор его подмодулей по включению является хорошо упорядоченным снизу.

LaTeX

$$$IsNoetherian(R,M) \iff WellFoundedGT(Submodule(R,M))$$$

Lean4

theorem isNoetherian_submodule_left {N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, (N ⊓ s).FG :=
  isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_left, fun H _ hs => inf_of_le_right hs ▸ H _⟩

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