English
For a simplex s and points p1,p2 with p1 in the affine span of the simplex, the squared distance from p1 to p2 equals the sum of the squared distances from p1 to the orthogonal projection of p2 onto s and from p2 to that projection.
Русский
Для члена выпуклого множества и точек выполняется соотношение квадратов расстояний, разложение по ортогональной проекции.
LaTeX
$$$$\operatorname{dist}(p_1, p_2)^2 = \operatorname{dist}(p_1, \mathrm{Proj}_s(p_2))^2 + \operatorname{dist}(p_2, \mathrm{Proj}_s(p_2))^2.$$$$
Lean4
/-- Reflecting an orthogonal vector plus a point in the subspace
produces the negation of that vector plus the point. -/
theorem reflection_orthogonal_vadd {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] {p : P}
(hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) : reflection s (v +ᵥ p) = -v +ᵥ p :=
by
rw [reflection_apply, orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]
simp
