iSup_toSubmodule_eq_top — Mathlib

English

iSup of LieSubmodules equals top iff iSup of underlying Submodules equals top.

Русский

iSup Ли-подмодулей равно топу тогда и только тогда, когда iSup их подмодулей равно топу.

LaTeX

$$$\iSup i, N_i = \top \;\Longleftrightarrow\; \iSup i, (N_i : Submodule R M) = \top$$$

Lean4

@[simp]
theorem iSup_toSubmodule_eq_top {ι : Sort*} {N : ι → LieSubmodule R L M} :
    ⨆ i, (N i : Submodule R M) = ⊤ ↔ ⨆ i, N i = ⊤ := by
  rw [← iSup_toSubmodule, ← top_toSubmodule (L := L), toSubmodule_inj]

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