ι : Type ?u.21212445
𝕜 : Type ?u.21212448
E : Type ?u.21212451
F : Type ?u.21212454
A : Type ?u.21212457
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ g x
H : ∀ (x : ℝ), x ∈ Ioc a b → f x ≤ g x := fun x hx => h x (Ioc_subset_Icc_self hx)
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
ι : Type ?u.21212445
𝕜 : Type ?u.21212448
E : Type ?u.21212451
F : Type ?u.21212454
A : Type ?u.21212457
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ g x
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
let H x hx := h x <| Ioc_subset_Icc_self hx
no goals
ι : Type ?u.21212445
𝕜 : Type ?u.21212448
E : Type ?u.21212451
F : Type ?u.21212454
A : Type ?u.21212457
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ g x
H : ∀ (x : ℝ), x ∈ Ioc a b → f x ≤ g x := fun x hx => h x (Ioc_subset_Icc_self hx)
⊢ (∫ (u : ℝ) in a..b, f u ∂μ) ≤ ∫ (u : ℝ) in a..b, g u ∂μ
simpa only [integral_of_le hab] using set_integral_mono_on hf.1 hg.1 measurableSet_Ioc H