sSup_simples_le — Mathlib

English

Let M be a semisimple module over a ring R. For every submodule N of M, the supremum of all simple submodules contained in N equals N.

Русский

Пусть M образует полупрямой модуль над кольцом R. Для любого подмодуля N модуля M наибольший верхний предел простых подмодулей, лежащих внутри N, равен N.

LaTeX

$$$\IsSemisimpleModule\ R\ M\Rightarrow \forall N : Submodule R\ M, \mathrm{sSup}\{m : Submodule R\ M \mid IsSimpleModule R m \land m \le N\} = N$$$

Lean4

theorem sSup_simples_le (N : Submodule R M) : sSup {m : Submodule R M | IsSimpleModule R m ∧ m ≤ N} = N := by
  simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_le_eq _

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