f✝ f : StieltjesFunction
x : ℝ
⊢ (⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r) = ⨅ (r : ↑(Ioi x)), ↑f ↑r
f✝ f : StieltjesFunction
x : ℝ
⊢ (⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r) = ↑f x
rw [← iInf_Ioi_eq f x]
f✝ f : StieltjesFunction
x : ℝ
⊢ BddBelow (↑f '' Ioi x)
f✝ f : StieltjesFunction
x : ℝ
⊢ (⨅ (r : { r' // x < ↑r' }), ↑f ↑↑r) = ⨅ (r : ↑(Ioi x)), ↑f ↑r
refine' (iInf_Ioi_eq_iInf_rat_gt _ _ f.mono).symm
f✝ f : StieltjesFunction
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y
f✝ f : StieltjesFunction
x : ℝ
⊢ BddBelow (↑f '' Ioi x)
refine' ⟨f x, fun y => _⟩
case intro.intro
f✝ f : StieltjesFunction
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y
f✝ f : StieltjesFunction
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y
rintro ⟨y, hy_mem, rfl⟩
no goals
case intro.intro
f✝ f : StieltjesFunction
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y
exact f.mono (le_of_lt hy_mem)