∀ {α : Type u_1} {E : Type u_2} {F' : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F') {C : ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) →
    ∀ (f : MeasureTheory.SimpleFunc α E),
      MeasureTheory.Integrable (⇑f) μ →
        ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖