English
Reflecting a point obtained by moving along an orthogonal direction from p preserves the opposite vector direction, giving the reflected point.
Русский
Отражение точки, полученной добавлением ортогонального вектора к p, меняет направление вектора на противоположное и сохраняет положение по основанию p.
LaTeX
$$$$\mathrm{reflection}_s(p +_V) = -V + p$$$$
Lean4
/-- Reflecting a vector plus a point in the subspace produces the
negation of that vector plus the point if the vector is a multiple of
the result of subtracting a point's orthogonal projection from that
point. -/
theorem reflection_vadd_smul_vsub_orthogonalProjection {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : ℝ) (hp₁ : p₁ ∈ s) :
reflection s (r • (p₂ -ᵥ orthogonalProjection s p₂) +ᵥ p₁) = -(r • (p₂ -ᵥ orthogonalProjection s p₂)) +ᵥ p₁ :=
reflection_orthogonal_vadd hp₁ (Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal s _))
