iSupIndep_toSubmodule — Mathlib

English

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

Русский

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

LaTeX

$$$\bigl(\iSup i, N_i^{\text{submodule}}\bigr) = \top \;\Longleftrightarrow\; \iSup i, N_i = \top$$$

Lean4

@[simp]
theorem iSupIndep_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
    iSupIndep (fun i ↦ (N i : Submodule R M)) ↔ iSupIndep N := by simp [iSupIndep_def, ← disjoint_toSubmodule]

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