set_has_minimal — Mathlib

English

If M is Artinian, then every nonempty set of submodules has a minimal member.

Русский

Пусть M артинанов; тогда любая ненулевая непустая совокупность подмодулей имеет минимальный элемент.

LaTeX

$$$[IsArtinian\\ R\\ M] \\Rightarrow (a.Nonempty \\Rightarrow \\exists M' \\in a, \\forall I \\in a, \\neg(I < M'))$$$

Lean4

theorem set_has_minimal [IsArtinian R M] (a : Set <| Submodule R M) (ha : a.Nonempty) : ∃ M' ∈ a, ∀ I ∈ a, ¬I < M' :=
  set_has_minimal_iff_artinian.mpr ‹_› a ha

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