set_has_minimal_iff_artinian — Mathlib

English

An Artinian module is characterized by the property that every nonempty set of submodules contains a minimal element.

Русский

Артинов модуль характеризуется тем, что каждая ненулевая непустая совокупность подмодулей содержит минимальный элемент.

LaTeX

$$$(\\forall a: Set\\ Submodule\\ R M), a.Nonempty \\Rightarrow \\exists M' \\in a, \\forall I \\in a, \\neg(I < M')$$$

Lean4

/-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them. -/
theorem set_has_minimal_iff_artinian :
    (∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M := by
  rw [isArtinian_iff, WellFounded.wellFounded_iff_has_min]

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