instCompleteLattice — Mathlib

English

Two Lie submodules are complementary iff their underlying Submodules are complementary.

Русский

Два подподмодуля Ли комплементарны тогда и только тогда, когда их подмодули как обычные подмодули комплементарны друг другу.

LaTeX

$$$\text{IsCompl}(N,N') \;\Longleftrightarrow\; \text{IsCompl}(N^{\text{toSubmodule}}, N'^{\text{toSubmodule}})$$$

Lean4

/-- The set of Lie submodules of a Lie module form a complete lattice. -/
instance : CompleteLattice (LieSubmodule R L M) :=
  {
    toSubmodule_injective.completeLattice toSubmodule sup_toSubmodule inf_toSubmodule sSup_toSubmodule_eq_iSup
      sInf_toSubmodule_eq_iInf rfl rfl with
    toPartialOrder := SetLike.instPartialOrder }

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