theorem projectionPoint_toSetValuedOperator_isMaximallyMonotone_of_nonempty_isClosed_convex {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {C : Set H} (hC_nonempty : C.Nonempty) (hC_closed : IsClosed C) (hC_convex : Convex ℝ C) : Maximal SetValuedOperator.IsMonotone (Function.toSetValuedOperator P[C, ⋯])

Example 20.32: the metric projection onto a nonempty closed convex subset of a real Hilbert space is maximally monotone when viewed as its associated singleton-valued set-valued operator.