ι : Type ?u.8489962
𝕜 : Type ?u.8489965
E : Type u_1
F : Type ?u.8489971
A : Type ?u.8489974
inst✝⁴ : NormedAddCommGroup E
μ : MeasureTheory.Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b)
ι : Type ?u.8489962
𝕜 : Type ?u.8489965
E : Type u_1
F : Type ?u.8489971
A : Type ?u.8489974
inst✝⁴ : NormedAddCommGroup E
μ : MeasureTheory.Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntervalIntegrable u μ a b
rw [intervalIntegrable_iff]
no goals
ι : Type ?u.8489962
𝕜 : Type ?u.8489965
E : Type u_1
F : Type ?u.8489971
A : Type ?u.8489974
inst✝⁴ : NormedAddCommGroup E
μ : MeasureTheory.Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b)
exact (hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self