theorem SetValuedOperator.Maximal.inverse {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {A : SetValuedOperator H H} (hA : Maximal IsMonotone A) : Maximal IsMonotone A.inverse

Proposition 20.22 (1): the inverse of a maximally monotone set-valued operator is maximally monotone.

theorem SetValuedOperator.Maximal.output_translation_smul_input_translation {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {A : SetValuedOperator H H} (hA : Maximal IsMonotone A) (z u : H) (γ : ↑(Set.Ioi 0)) : Maximal IsMonotone ((Function.toSetValuedOperator fun (x : H) => u) + ↑γ • A.translate (-z))

Proposition 20.22 (2): for z, u : H and γ ∈ ℝ_{++}, the affine perturbation x ↦ {u} + γ • A (x + z) of a maximally monotone operator is maximally monotone.