theorem metricProjection_firmly_nonexpansive {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) (v w : E) : inner ℝ (projectionPoint C hC_nonempty hC_closed hC_convex v - projectionPoint C hC_nonempty hC_closed hC_convex w) (v - w) ≥ ‖projectionPoint C hC_nonempty hC_closed hC_convex v - projectionPoint C hC_nonempty hC_closed hC_convex w‖ ^ 2

Theorem 5.4 (1): the point projection onto a nonempty closed convex set in a complete real inner product space, hence in particular in a Euclidean space, is firmly nonexpansive.

theorem projectionPoint_norm_sub_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) (x y : E) : ‖projectionPoint C hC_nonempty hC_closed hC_convex x - projectionPoint C hC_nonempty hC_closed hC_convex y‖ ≤ ‖x - y‖

Helper for Theorem 5.4: the point projection is pointwise nonexpansive in norm.

theorem metricProjection_nonexpansive {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : Set E) (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) : LipschitzWith 1 (projectionPoint C hC_nonempty hC_closed hC_convex)

Theorem 5.4 (2): the point projection onto a nonempty closed convex set in a complete real inner product space, hence in particular in a Euclidean space, is nonexpansive in the canonical LipschitzWith 1 form.