theorem
ERealFunction.subdifferential_isMaximallyMonotone_of_mem_gammaZero
{H : Type u}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
{f : H → ↑(Set.Ioi ⊥)}
(hf : f ∈ Γ₀(H))
:
Maximal SetValuedOperator.IsMonotone (subdifferential f)
Theorem 20.25: (Moreau) if f ∈ Γ₀(H), then the subdifferential ∂ f is maximally
monotone.