Theorem EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq

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_sup_of_orthogonalProjection_eqView on Github →
2025-10-28 05:30
Mathlib/Geometry/Euclidean/Projection.lean
feat(Geometry/Euclidean/Projection): projection onto sup (#30703) …
Added EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eqView on Github →