submodule_span_le_lieSpan

Mathlib.Algebra.Lie.Subalgebra

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

English

For every LieSubalgebra K of L, lieSpan_R L s ≤ K if and only if s ⊆ K.

Русский

Для любой подпалгебры K L, lieSpan_R L s ≤ K тогда и только тогда, когда s ⊆ K.

LaTeX

$$$\\operatorname{lieSpan}_R L(s) \\le K \\iff s \\subseteq K$$$

Lean4

theorem submodule_span_le_lieSpan : Submodule.span R s ≤ lieSpan R L s :=
  by
  rw [Submodule.span_le, coe_toSubmodule]
  apply subset_lieSpan

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

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

Разделы

Аффилиация

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