E : Type ?u.158221
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
E : Type ?u.158221
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
refine integrableOn_Ioi_deriv_of_nonneg (fun x hx ↦ ?_) (fun x hx => hderiv x hx.out.le) g'pos hg
no goals
E : Type ?u.158221
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt g (g' x) x
g'pos : ∀ (x : ℝ), x ∈ Ioi a → 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
exact (hderiv x hx).continuousAt.continuousWithinAt