English
A module M is Noetherian if and only if every nonempty set of submodules has a maximal submodule under inclusion.
Русский
Модуль M Нётеров тогда и только тогда, когда любою непустой множеству подмодулей существует максимальный подмодуль по включению.
LaTeX
$$$(\\forall a \\subseteq \\mathrm{Submodule}_R(M))\, (a \\neq \\varnothing \\Rightarrow \\exists M' \\in a\\, \\forall I \\in a, \\neg (M' < I)) \\ \\iff \\ \\operatorname{IsNoetherian}(R,M)$$$
Lean4
/-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
-/
theorem set_has_maximal_iff_noetherian :
(∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M := by
rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]
