Theorem AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection

Modification history

2025-09-01 07:30
Mathlib/Geometry/Euclidean/SignedDist.lean
feat(Geometry/Euclidean/SignedDist): `signedDist` between two points (#27260) …
Added AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjectionView on Github →