Commit 2025-02-16 02:27 41fdb023

feat(Geometry/Euclidean/Basic): distance between point and affine subspace equals distance to orthogonal projection (#21604) Show that the distance between a point and an affine subspace given with dist p (orthogonalProjection s p) equals that given with Metric.infDist. I have not however tried to work out which existing lemmas might most appropriately be restated with Metric.infDist and which are more useful in the orthogonalProjection form.