theorem setValuedProjector_isMaximallyMonotone_of_isChebyshev {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H] {C : Set H} (hC : IsChebyshev C) : Maximal SetValuedOperator.IsMonotone P[C]

Example 20.33: in a finite-dimensional real Hilbert space, the set-valued projector P[C] onto a Chebyshev set is maximally monotone.