English
If a property p holds for all simple reflections, holds for the identity, and is preserved under multiplication, then p holds for all elements of W.
Русский
Если свойство p выполняется для всех простых отражений, для единицы и сохраняется при умножении, то p выполняется для всех элементов W.
LaTeX
$$p(w) holds if p(s_i) for all i, p(1), and closure under multiplication$$
Lean4
/-- If `p : W → Prop` holds for all simple reflections, it holds for the identity, and it is
preserved under multiplication, then it holds for all elements of `W`. -/
theorem simple_induction {p : W → Prop} (w : W) (simple : ∀ i : B, p (s i)) (one : p 1)
(mul : ∀ w w' : W, p w → p w' → p (w * w')) : p w :=
by
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
exact Submonoid.closure_induction (fun x ⟨i, hi⟩ ↦ hi ▸ simple i) one (fun _ _ _ _ ↦ mul _ _) this
