English
Two points p1, p2 in s are equidistant to p3 iff their projections are equally distant from p3.
Русский
Две точки p1, p2 в s равны по расстоянию до p3 тогда и только тогда, когда их проекции на s имеют одинаковое расстояние до p3.
LaTeX
$$$ dist p_1 p_3 = dist p_2 p_3 \iff dist p_1 (\operatorname{orthogonalProjection} s p_3) = dist p_2 (\operatorname{orthogonalProjection} s p_3) $$$
Lean4
/-- `p` is equidistant from two points in `s` if and only if its
`orthogonalProjection` is. -/
theorem dist_eq_iff_dist_orthogonalProjection_eq {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {p₁ p₂ : P} (p₃ : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
dist p₁ p₃ = dist p₂ p₃ ↔ dist p₁ (orthogonalProjection s p₃) = dist p₂ (orthogonalProjection s p₃) :=
by
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, ← mul_self_inj_of_nonneg dist_nonneg dist_nonneg,
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₁,
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₂]
simp
