sSup_toSubmodule_eq_iSup — Mathlib

English

The underlying Submodule of the supremum over a set S equals the iterated supremum over all elements N ∈ S of their underlying Submodules.

Русский

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

LaTeX

$$$\left( \mathrm{sSup} S \right)^{\text{toSubmodule}} = \bigl(\forall N \in S \bigr) \bigvee_{N \in S} (N^{\text{toSubmodule}})$$$

Lean4

theorem sSup_toSubmodule_eq_iSup (S : Set (LieSubmodule R L M)) :
    (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (N : Submodule R M) := by rw [sSup_toSubmodule, ← Set.image, sSup_image]

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