English
Let R be a ring, L a Lie algebra over R, and s a subset of L. Then lieSpan_R L s is the smallest Lie subalgebra of L containing s; equivalently, for any Lie subalgebra N of L that contains s, lieSpan_R L s is contained in N.
Русский
Пусть R — кольцо, L — алгебра Ли над R, и s — подмножество L. Тогда lieSpan_R L s является наименьшей подалгеброй Ли в L, содержащей s; эквивалентно: для любой подпалгебры N ⊆ L, содержащей s, верно lieSpan_R L s ⊆ N.
LaTeX
$$$\\operatorname{lieSpan}_R L(s)=\\bigcap\\{N\\le L\\mid s\\subseteq N\\}$$$
Lean4
/-- The Lie subalgebra of a Lie algebra `L` generated by a subset `s ⊆ L`. -/
def lieSpan : LieSubalgebra R L :=
sInf {N | s ⊆ N}
