English
There is an induction principle for the Weyl group: if a property holds for all simple reflections, holds for the identity, and is preserved under multiplication, then it holds for every element of the Weyl group.
Русский
Существует принцип индукции для Weyl-группы: если свойство выполняется для всех простых отражений, для единицы и сохраняется при умножении, то оно выполняется для каждого элемента Weyl-группы.
LaTeX
$$$\\forall{pred},\\;\\Big(\\forall i,\\ pred(\\operatorname{Equiv.reflection}(P,i),\\; P. reflection\\_mem\\_weylGroup i)\\Big) \\\\land pred(1,\\; one\\_mem) \\\\land \\Big(\\forall x,y, hx,hy,\\pred x hx \\to \\pred y hy \\to \\pred(x\\cdot y) (mul\\_mem hx hy)\\Big) \\Rightarrow \\forall {x}, x\\in P.weylGroup, pred x hx.$$
Lean4
@[elab_as_elim]
theorem induction {pred : (g : Aut P) → g ∈ P.weylGroup → Prop}
(mem : ∀ i, pred (Equiv.reflection P i) (P.reflection_mem_weylGroup i)) (one : pred 1 (one_mem _))
(mul : ∀ x y hx hy, pred x hx → pred y hy → pred (x * y) (mul_mem hx hy)) {x} (hx : x ∈ P.weylGroup) : pred x hx :=
by
let pred' : (g : Aut P) → g ∈ Submonoid.closure (range (Equiv.reflection P)) → Prop := fun g hg ↦
pred g <| by change g ∈ P.weylGroup.toSubmonoid; rwa [weylGroup_toSubmonoid]
have hx' : x ∈ Submonoid.closure (range (Equiv.reflection P)) := by rwa [← weylGroup_toSubmonoid]
suffices pred' x hx' from this
apply Submonoid.closure_induction
· rintro - ⟨i, rfl⟩
exact mem i
· exact one
· intro x y hx hy hx' hy'
rw [← weylGroup_toSubmonoid] at hx hy
exact mul x y hx hy hx' hy'
