English
The square distance between two points obtained by adding scalar multiples of the same orthogonal vector to points in the same subspace satisfies a Pythagoras-type identity.
Русский
Квадрат расстояния между точками, полученными добавлением скалярных кратных одного и того же ортогонального вектора к точкам внутри одного подпространства, удовлетворяет некоему тождеству Пифагора.
LaTeX
$$$ dist(r_1 v + p_1, r_2 v + p_2)^2 = dist(p_1,p_2)^2 + (r_1 - r_2)^2 \|v\|^2 $$$
Lean4
/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector was
in the orthogonal direction. -/
theorem orthogonalProjection_vadd_eq_self {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection]
{p : P} (hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) : orthogonalProjection s (v +ᵥ p) = ⟨p, hp⟩ :=
by
have h := vsub_orthogonalProjection_mem_direction_orthogonal s (v +ᵥ p)
rw [vadd_vsub_assoc, Submodule.add_mem_iff_right _ hv] at h
refine (eq_of_vsub_eq_zero ?_).symm
ext
refine Submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ ?_ h
exact (_ : s.direction).2
