sSup_toSubmodule — Mathlib

English

The underlying Submodule of the supremum sSup S equals the supremum (join) of the underlying Submodules of elements of S.

Русский

Основанный на подпроцедуре верхний предел множества S совпадает с верхней гранью подмодулей элементов S.

LaTeX

$$$\uparrow(\mathrm{sSup} S) = \mathrm{sSup}\{(s : Submodule R M) \mid s \in S\}$$$

Lean4

@[simp]
theorem sSup_toSubmodule (S : Set (LieSubmodule R L M)) :
    (↑(sSup S) : Submodule R M) = sSup ({(s : Submodule R M) | s ∈ S}) :=
  rfl

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