English
A point is equidistant from a set ps iff its projection is equidistant from the projection of the set.
Русский
Точка поровну удалена от множества ps тогда и только тогда, когда её проекция является равноудалённой от проекции множества.
LaTeX
$$$ dist\ Set.ps \; fun p => dist p1 p = dist p2 p \iff dist p1 (orthogonalProjection s p) = dist p2 (orthogonalProjection s p) $$$
Lean4
/-- `p` is equidistant from a set of points in `s` if and only if its
`orthogonalProjection` is. -/
theorem dist_set_eq_iff_dist_orthogonalProjection_eq {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {ps : Set P} (hps : ps ⊆ s) (p : P) :
(Set.Pairwise ps fun p₁ p₂ => dist p₁ p = dist p₂ p) ↔
Set.Pairwise ps fun p₁ p₂ => dist p₁ (orthogonalProjection s p) = dist p₂ (orthogonalProjection s p) :=
⟨fun h _ hp₁ _ hp₂ hne => (dist_eq_iff_dist_orthogonalProjection_eq p (hps hp₁) (hps hp₂)).1 (h hp₁ hp₂ hne),
fun h _ hp₁ _ hp₂ hne => (dist_eq_iff_dist_orthogonalProjection_eq p (hps hp₁) (hps hp₂)).2 (h hp₁ hp₂ hne)⟩
