no goals
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I J : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
c : ℝ
hc : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ‖f x‖ ≤ c
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ‖integral I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))‖ ≤ ENNReal.toReal (↑↑μ ↑I) * c
simpa only [integral_const] using norm_integral_le_of_norm_le hc μ (integrable_const c)