∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) {C : ℝ},
  (∀ (x : R), |↑f x| ≤ C) → ∀ (x : R), C + 1 ≤ ↑f x → ∃ u, Filter.Tendsto (↑f) Filter.atTop (nhds u)