ι : Type ?u.21446228
𝕜 : Type ?u.21446231
E : Type ?u.21446234
F : Type ?u.21446237
A : Type ?u.21446240
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
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc c d)] f
hfi : IntervalIntegrable f μ c d
⊢ (∫ (x : ℝ) in Ioc a b, f x ∂μ) ≤ ∫ (x : ℝ) in Ioc c d, f x ∂μ
ι : Type ?u.21446228
𝕜 : Type ?u.21446231
E : Type ?u.21446234
F : Type ?u.21446237
A : Type ?u.21446240
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
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc c d)] f
hfi : IntervalIntegrable f μ c d
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) ≤ ∫ (x : ℝ) in c..d, f x ∂μ
rw [integral_of_le hab, integral_of_le (hca.trans (hab.trans hbd))]
no goals
ι : Type ?u.21446228
𝕜 : Type ?u.21446231
E : Type ?u.21446234
F : Type ?u.21446237
A : Type ?u.21446240
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
c d : ℝ
hca : c ≤ a
hab : a ≤ b
hbd : b ≤ d
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc c d)] f
hfi : IntervalIntegrable f μ c d
⊢ (∫ (x : ℝ) in Ioc a b, f x ∂μ) ≤ ∫ (x : ℝ) in Ioc c d, f x ∂μ
exact set_integral_mono_set hfi.1 hf (Ioc_subset_Ioc hca hbd).eventuallyLE