lie_mem

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.lie_mem

English

If x,y ∈ L', then [x,y] ∈ L' (closure under bracket).

Русский

Если x,y ∈ L', то [x,y] ∈ L' (замыкание по бракету).

LaTeX

$$$x,y \in L' \Rightarrow [x,y] \in L'$$$

Lean4

theorem lie_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (⁅x, y⁆ : L) ∈ L' :=
  L'.lie_mem' hx hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru