α : Type u_1
E : Type u_2
F : Type ?u.205081
𝕜 : Type ?u.205084
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.205186
F' : Type ?u.205189
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ ‖weightedSMul μ s‖ ≤ 1 * ENNReal.toReal (↑↑μ s)
α : Type u_1
E : Type u_2
F : Type ?u.205081
𝕜 : Type ?u.205084
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.205186
F' : Type ?u.205189
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α →ₛ E
hf : Integrable ↑f
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)
refine' (norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => _) hf).trans (one_mul _).le
no goals
α : Type u_1
E : Type u_2
F : Type ?u.205081
𝕜 : Type ?u.205084
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.205186
F' : Type ?u.205189
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α →ₛ E
hf : Integrable ↑f
s : Set α
x✝¹ : MeasurableSet s
x✝ : ↑↑μ s < ⊤
⊢ ‖weightedSMul μ s‖ ≤ 1 * ENNReal.toReal (↑↑μ s)
exact (norm_weightedSMul_le s).trans (one_mul _).symm.le