Theorem EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le

Modification history

2025-12-11 08:08
Mathlib/Geometry/Euclidean/Projection.lean
refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces (#27378) …
Modified EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_leView on Github →
2025-10-28 05:30
Mathlib/Geometry/Euclidean/Projection.lean
feat(Geometry/Euclidean/Projection): `orthogonalProjection_orthogonalProjection_of_le` (#30474) …
Added EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_leView on Github →