English
Reflecting across a subspace is an involution; applying reflection twice returns the original point.
Русский
Отражение через подпространство — это инволютивное отображение: два отражения подряд возвращают исходную точку.
LaTeX
$$$$\mathrm{reflection}_s(\mathrm{reflection}_s(p)) = p.$$$$
Lean4
/-- Reflecting twice in the same subspace. -/
@[simp]
theorem reflection_reflection (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P) :
reflection s (reflection s p) = p :=
by
have :
∀ a : s,
∀ b : V, s.direction.orthogonalProjection b = 0 → reflection s (reflection s (b +ᵥ (a : P))) = b +ᵥ (a : P) :=
by
intro _ _ h
simp [reflection]
rw [← vsub_vadd p (orthogonalProjection s p)]
exact this (orthogonalProjection s p) _ (orthogonalProjection_vsub_orthogonalProjection s p)
