theorem ERealFunction.subdifferential_isMonotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain f).Nonempty) : (subdifferential f).IsMonotone

Example 20.3: for an ]-∞,+∞]-valued function with nonempty effective domain, the subdifferential is a monotone set-valued operator.