Commit 2025-10-28 05:30 5ab5c34b
View on Github →feat(Geometry/Euclidean/Projection): orthogonalProjection_orthogonalProjection_of_le (#30474)
Add a lemma that orthogonalProjection s₁ (orthogonalProjection s₂ p) = orthogonalProjection s₁ p for s₁ ≤ s₂. (A similar lemma for projection onto submodules rather than affine subspaces already exists.)