theorem mem_projection_mapping_iff_inner_le_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_convex : Convex ℝ C) (x : E) {u : E} (hu : u ∈ C) : u ∈ P[C] x ↔ ∀ y ∈ C, inner ℝ (x - u) (y - u) ≤ 0

Helper for Theorem 6.41: for a convex set C, a point u ∈ C belongs to the projection set P[C] x exactly when it satisfies the Hilbert-space variational inequality against every point of C.

theorem projection_mapping_eq_singleton_iff_inner_le_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Set E) (hC_convex : Convex ℝ C) (x : E) {u : E} (hu : u ∈ C) : P[C] x = {u} ↔ ∀ y ∈ C, inner ℝ (x - u) (y - u) ≤ 0

Theorem 6.41: second projection theorem. For a convex set C and a point u ∈ C, the equality P[C] x = {u} holds if and only if inner ℝ (x - u) (y - u) ≤ 0 for every y ∈ C. The usual nonempty and closed hypotheses are unnecessary for this variational characterization once a candidate point u ∈ C is fixed.