English
The Weyl group submonoid is generated by the reflections; in other words, the WeylGroup’s submonoid equals the closure of the range of the reflection map.
Русский
Подмножество Weyl-группы образуется генераторами‑отражениями; иными словами, подмонаид Weyl-группы равен замыканию множества отражений.
LaTeX
$$$ P.weylGroup.toSubmonoid = \\operatorname{Submonoid.closure}(\\operatorname{range}(\\operatorname{Equiv.reflection}(P))).$$$
Lean4
/-- Usually `RootPairing.weylGroup.induction` will be more useful than this lemma. -/
theorem weylGroup_toSubmonoid : P.weylGroup.toSubmonoid = Submonoid.closure (range (Equiv.reflection P)) :=
by
suffices range (Equiv.reflection P) = (range (Equiv.reflection P))⁻¹ by
rw [weylGroup, Subgroup.closure_toSubmonoid, ← this, union_self]
ext; simp [← inv_eq_iff_eq_inv]
