English
The union of the ranges of the sets HH, EF, HE, HF, adE, adF, which collects all Cartan relations inside the free Lie algebra on Cartan generators.
Русский
Объединение множеств образов HH, EF, HE, HF, adE, adF, объединяющее все реляции Картанa внутри свободной Ли-алгебры на генераторах Картанa.
LaTeX
$$$\\text{toSet } R\\; A = (\\mathrm{range}(HH R)) \\cup (\\mathrm{range}(EF R)) \\cup (\\mathrm{range}(HE R A)) \\cup (\\mathrm{range}(HF R A)) \\cup (\\mathrm{range}(adE R A)) \\cup (\\mathrm{range}(adF R A))$$$
Lean4
/-- The union of all the relations as a subset of the free Lie algebra. -/
def toSet [DecidableEq B] : Set (FreeLieAlgebra R (Generators B)) :=
(Set.range <| HH R) ∪ (Set.range <| EF R) ∪ (Set.range <| HE R A) ∪ (Set.range <| HF R A) ∪ (Set.range <| adE R A) ∪
(Set.range <| adF R A)
