theorem Function.id_add_smul_toSetValuedOperator_isMaximallyMonotone_of_nonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : H → H) (hT : LipschitzWith 1 T) {α : ℝ} (hα : α ∈ Set.Icc (-1) 1) : Maximal SetValuedOperator.IsMonotone (toSetValuedOperator (id + α • T))

Example 20.29: if T : H → H is nonexpansive and α ∈ [-1, 1], then the affine perturbation Id + α T, viewed as a singleton-valued set-valued operator, is maximally monotone.