@[simp]

theorem SetValuedOperator.add_smul_apply {X : Type u} {Y : Type v} [AddCommGroup Y] [Module ℝ Y] (A B : SetValuedOperator X Y) (c : ℝ) (x : X) : (A + c • B) x = A x + c • B x

Text 1.0.16: for set-valued operators A B : X → Set Y and a real scalar c (λ in the text), the linear combination A + λ B is the pointwise operator satisfying (A + c • B) x = A x + c • B x.