f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Iic x) = ofReal (↑f x - l)
refine' tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) _
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))
simp_rw [measure_Ioc]
no goals
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))
exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)