English
If a set s consists of indices i with j orthogonal to each i in s, then any x in span_R(P.root''s image of s) is fixed by reflection j.
Русский
Если s состоит из индексов i с ортогональностью по отношению к j, то любой x в span_R(P.root''s image of s) удовлетворяет, что reflection_j(x) = x.
LaTeX
$$$$ \\forall s, (\\forall i \\in s, P.IsOrthogonal j i) \\Rightarrow \\forall x \\in \\operatorname{span}_R(P.root''s\,image\,s),\\; P.reflection_j(x) = x. $$$$
Lean4
theorem isFixedPt_reflection_of_isOrthogonal {s : Set ι} (hj : ∀ i ∈ s, P.IsOrthogonal j i) {x : M}
(hx : x ∈ span R (P.root '' s)) : IsFixedPt (P.reflection j) x :=
by
rw [IsFixedPt]
induction hx using Submodule.span_induction with
| zero => rw [map_zero]
| add u v hu hv hu' hv' => rw [map_add, hu', hv']
| smul t u hu hu' => rw [map_smul, hu']
| mem u hu =>
obtain ⟨i, his, rfl⟩ := hu
exact IsOrthogonal.reflection_apply_right <| hj i his
