iSup_eq_top_iff_toSubmodule — Mathlib

English

Equivalence of iSup top for LieSubmodule and for Submodule.

Русский

Эквивалентность топа iSup для Ли-подмодулей и для подмодулей.

LaTeX

$$$\text{iSup}_{\text{LieSubmodule}} N = \top \;\Leftrightarrow\; \text{iSup}_{\textSubmodule} (N) = \top$$$

Lean4

@[deprecated iSup_toSubmodule_eq_top (since := "2025-04-03")]
theorem iSup_eq_top_iff_toSubmodule {ι : Sort*} {N : ι → LieSubmodule R L M} :
    ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ :=
  iSup_toSubmodule_eq_top.symm

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