sub_mem

Mathlib.Algebra.Lie.Subalgebra

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

English

If x,y ∈ L', then x - y ∈ L'.

Русский

Если x,y ∈ L', то x − y ∈ L'.

LaTeX

$$$x,y \in L' \Rightarrow x - y \in L'$$$

Lean4

protected theorem sub_mem {x y : L} : x ∈ L' → y ∈ L' → (x - y : L) ∈ L' :=
  sub_mem

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

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

Разделы

Аффилиация

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