English
Equality between the nonnegative distance and infNndist holds for the projection.
Русский
Равенство между неотрицательным расстоянием и infNndist для проекции держится.
LaTeX
$$$ dist p (\operatorname{orthogonalProjection} s p) = \operatorname{infNndist} p s $$$
Lean4
/-- The distance between a point and its orthogonal projection to a subspace equals the distance
to that subspace as given by `Metric.infDist`. This is not a `simp` lemma since the simplest form
depends on the context (if any calculations are to be done with the distance, the version with
the orthogonal projection gives access to more lemmas about orthogonal projections that may be
useful). -/
theorem dist_orthogonalProjection_eq_infDist (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection]
(p : P) : dist p (orthogonalProjection s p) = Metric.infDist p s :=
by
refine le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))
rw [Metric.infDist_eq_iInf]
refine le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg
rw [dist_comm _ (x : P)]
simp_rw [pow_two, dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p x.property]
simp [mul_self_nonneg]
