α : Type u_1
β : Type ?u.290238
E : Type ?u.290241
F : Type ?u.290244
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s t : Set α
hf✝ : IntegrableOn f s
hg : IntegrableOn g s
c : ℝ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
hf : ∀ (x : α), x ∈ s → c ≤ f x
hfint : IntegrableOn (fun x => f x) s
⊢ (∫ (x : α) in s, c ∂μ) ≤ ∫ (x : α) in s, f x ∂μ
α : Type u_1
β : Type ?u.290238
E : Type ?u.290241
F : Type ?u.290244
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s t : Set α
hf✝ : IntegrableOn f s
hg : IntegrableOn g s
c : ℝ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
hf : ∀ (x : α), x ∈ s → c ≤ f x
hfint : IntegrableOn (fun x => f x) s
⊢ c * ENNReal.toReal (↑↑μ s) ≤ ∫ (x : α) in s, f x ∂μ
rw [mul_comm, ← smul_eq_mul, ← set_integral_const c]
no goals
α : Type u_1
β : Type ?u.290238
E : Type ?u.290241
F : Type ?u.290244
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s t : Set α
hf✝ : IntegrableOn f s
hg : IntegrableOn g s
c : ℝ
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
hf : ∀ (x : α), x ∈ s → c ≤ f x
hfint : IntegrableOn (fun x => f x) s
⊢ (∫ (x : α) in s, c ∂μ) ≤ ∫ (x : α) in s, f x ∂μ
exact set_integral_mono_on (integrableOn_const.2 (Or.inr hμs.lt_top)) hfint hs hf