f✝ f : StieltjesFunction
x : ℝ
⊢ ContinuousWithinAt (↑f) (Ici x) x
f✝ f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ↑f x
rw [← f.mono.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_Ioi_iff_Ici]
no goals
f✝ f : StieltjesFunction
x : ℝ
⊢ ContinuousWithinAt (↑f) (Ici x) x
exact f.right_continuous' x