reflection_apply — Mathlib

English

The reflection of a point p across an affine subspace s is given by the projection of p onto s, moved by the excess from p to the projection. Equivalently, refl_s(p) = 2 Proj_s(p) − p.

Русский

Отражение точки p относительно аффинного подпространства s задаётся как отражение через проекцию: refl_s(p) = 2Proj_s(p) − p.

LaTeX

$$$$\operatorname{reflection}_s(p) = 2\operatorname{Proj}_s(p) - p.$$$$

Lean4

/-- The result of reflecting. -/
theorem reflection_apply (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P) :
    reflection s p = (↑(orthogonalProjection s p) -ᵥ p) +ᵥ (orthogonalProjection s p : P) :=
  rfl

Похожие утверждения