English
The lieSpan operation and the inclusion of Lie subalgebras form a Galois connection: for all s ⊆ L and K ≤ L, lieSpan_R L(s) ≤ K iff s ⊆ K.
Русский
Операции lieSpan и включение подпалгебр Ли образуют систему Галуа: для любых s ⊆ L и K ≤ L выполняется lieSpan_R L(s) ≤ K тогда и только тогда s ⊆ K.
LaTeX
$$$\\forall s\\subseteq L,\\forall K:\\text{LieSubalgebra}_R L,\\ \\operatorname{lieSpan}_R L(s) \\le K \\iff s \\subseteq K$$$
Lean4
/-- `lieSpan` forms a Galois insertion with the coercion from `LieSubalgebra` to `Set`. -/
protected def gi : GaloisInsertion (lieSpan R L : Set L → LieSubalgebra R L) (↑)
where
choice s _ := lieSpan R L s
gc _ _ := lieSpan_le
le_l_u _ := subset_lieSpan
choice_eq _ _ := rfl
