add_eq_sup — Mathlib

English

Let N and N' be Lie submodules of M. Then their sum N + N' coincides with the supremum N ⊔ N' in the lattice of Lie submodules.

Русский

Пусть N и N' — подмодули Ли структуры на M. Тогда их сумма N + N' совпадает с их наибольшей верхней гранью N ⊔ N' в решётке подмодулей.

LaTeX

$$$N + N' = N \\sqcup N'$$$

Lean4

@[simp]
theorem add_eq_sup : N + N' = N ⊔ N' :=
  rfl

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