ι : Type ?u.20278930
𝕜 : Type ?u.20278933
E : Type ?u.20278936
F : Type ?u.20278939
A : Type ?u.20278942
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Icc a b)] f
H : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ioc a b), OfNat.ofNat 0 x ≤ f x :=
  ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
ι : Type ?u.20278930
𝕜 : Type ?u.20278933
E : Type ?u.20278936
F : Type ?u.20278939
A : Type ?u.20278942
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Icc a b)] f
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
let H := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
no goals
ι : Type ?u.20278930
𝕜 : Type ?u.20278933
E : Type ?u.20278936
F : Type ?u.20278939
A : Type ?u.20278942
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Icc a b)] f
H : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ioc a b), OfNat.ofNat 0 x ≤ f x :=
  ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
simpa only [integral_of_le hab] using set_integral_nonneg_of_ae_restrict H