English
The nonnegative distance to the projection is preserved and nonnegative.
Русский
Неотрицательное расстояние до проекции сохраняется и неотрицательно.
LaTeX
$$$ \operatorname{dist}_{+} p (\operatorname{orthogonalProjection} s p) \ge 0 $$$
Lean4
/-- The nonnegative distance between a point and its orthogonal projection to a subspace equals
the distance to that subspace as given by `Metric.infNndist`. 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_infNndist (s : AffineSubspace ℝ P) [Nonempty s]
[s.direction.HasOrthogonalProjection] (p : P) : nndist p (orthogonalProjection s p) = Metric.infNndist p s :=
by
rw [← NNReal.coe_inj]
simp [dist_orthogonalProjection_eq_infDist]
