Commit 2025-10-27 15:32 502d38e8

feat(Geometry/Euclidean/Projection): characteristic property (#30698) Add a lemma

lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p q : P} :
    orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by

that gives the characteristic property of the orthogonal projection in a more convenient form to use than the existing inter_eq_singleton_orthogonalProjection (from which it is derived). Deduce a lemma orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem about equality of two projections onto the same subspace.