iSup_toSubmodule — Mathlib

English

The supremum of LieSubmodules corresponds to the supremum of their underlying Submodules.

Русский

Супремум Ли-подмодулей соответствует супремуму их подмодулей как подмножеств.

LaTeX

$$$\bigl(\iSup i, p_i\bigr)^{\text{toSubmodule}} = \iSup i, (p_i^{\text{toSubmodule}})$$$

Lean4

@[simp]
theorem iSup_toSubmodule {ι} (p : ι → LieSubmodule R L M) :
    (↑(⨆ i, p i) : Submodule R M) = ⨆ i, (p i : Submodule R M) := by rw [iSup, sSup_toSubmodule]; ext;
  simp [Submodule.mem_sSup, Submodule.mem_iSup]

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