f✝ f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ⨅ (r : ↑(Ioi x)), ↑f ↑r
f✝ f : StieltjesFunction
x : ℝ
⊢ (⨅ (r : ↑(Ioi x)), ↑f ↑r) = ↑f x
suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]
f✝ f : StieltjesFunction
x : ℝ
⊢ 𝓝[Ioi x] x ≠ ⊥
f✝ f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ⨅ (r : ↑(Ioi x)), ↑f ↑r
rw [rightLim_eq_sInf f.mono, sInf_image']
f✝ f : StieltjesFunction
x : ℝ
⊢ NeBot (𝓝[Ioi x] x)
f✝ f : StieltjesFunction
x : ℝ
⊢ 𝓝[Ioi x] x ≠ ⊥
rw [← neBot_iff]
no goals
f✝ f : StieltjesFunction
x : ℝ
⊢ NeBot (𝓝[Ioi x] x)
infer_instance
no goals
f✝ f : StieltjesFunction
x : ℝ
this : rightLim (↑f) x = ⨅ (r : ↑(Ioi x)), ↑f ↑r
⊢ (⨅ (r : ↑(Ioi x)), ↑f ↑r) = ↑f x
rw [← this, f.rightLim_eq]