English
Let s be a nonempty affine subspace of P that admits an orthogonal projection. For a fixed subset ps of P contained in s, there exists a real number r such that every point p1 in ps is at distance r from p if and only if there exists a (possibly different) real number r such that every p1 in ps is at distance r from the orthogonal projection of p onto s.
Русский
Пусть s — непустое аффинное подпространство пространства P, для которого существует ортогональная проекция. Для фиксированного множества ps ⊆ s существует число r such that все p1 ∈ ps удовлетворяют dist(p1, p) = r, если и только если существует (возможно другое) число r such that для всех p1 ∈ ps выполняется dist(p1, Proj_s(p)) = r.
LaTeX
$$$$\exists r \in \mathbb{R}: \forall p_1 \in ps,\ dist(p_1, p) = r \ \Longleftrightarrow\ \exists r' \in \mathbb{R}: \forall p_1 \in ps,\ dist\bigl(p_1, \operatorname{Proj}_s(p)\bigr) = r'.$$$$
Lean4
/-- There exists `r` such that `p` has distance `r` from all the
points of a set of points in `s` if and only if there exists (possibly
different) `r` such that its `orthogonalProjection` has that distance
from all the points in that set. -/
theorem exists_dist_eq_iff_exists_dist_orthogonalProjection_eq {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {ps : Set P} (hps : ps ⊆ s) (p : P) :
(∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑(orthogonalProjection s p) = r :=
by
have h := dist_set_eq_iff_dist_orthogonalProjection_eq hps p
simp_rw [Set.pairwise_eq_iff_exists_eq] at h
exact h
