theorem IsProjectionPointOn.dist_le_dist {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Q : Set E} (hQ_convex : Convex ℝ Q) {x₁ p₁ x₂ p₂ : E} (hp₁ : IsProjectionPointOn Q x₁ p₁) (hp₂ : IsProjectionPointOn Q x₂ p₂) : dist p₁ p₂ ≤ dist x₁ x₂

Any two projection points onto a convex set are at most as far apart as their base points.

theorem IsProjectionPointOn.lipschitzWith {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Q : Set E} (hQ_convex : Convex ℝ Q) {projQ : E → E} (hproj : ∀ (x : E), IsProjectionPointOn Q x (projQ x)) : LipschitzWith 1 projQ

Any projection selector on a convex set is nonexpansive, recorded in the canonical map-level form LipschitzWith 1.

theorem euclideanProjection_nonexpansive {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : Set E) (hQ_nonempty : Q.Nonempty) (hQ_closed : IsClosed Q) (hQ_convex : Convex ℝ Q) : LipschitzWith 1 (euclideanProjection Q hQ_nonempty hQ_closed hQ_convex)

Theorem 2.34: the Euclidean projection onto a nonempty closed convex set in a complete real inner product space is nonexpansive, recorded in the canonical map-level form LipschitzWith 1. The textbook Euclidean-space statement is the specialization to ℝⁿ.