Continuity points of a Stieltjes function

A Stieltjes function is continuous exactly where its measure has no atom. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Stieltjes.lean.

theorem StieltjesFunction.continuousAt_iff_measure_singleton {R : Type u_1} [LinearOrder R] [TopologicalSpace R] [OrderTopology R] [CompactIccSpace R] [MeasurableSpace R] [BorelSpace R] [SecondCountableTopology R] [DenselyOrdered R] (f : StieltjesFunction R) {x : R} : ContinuousAt (↑f) x ↔ f.measure {x} = 0

A Stieltjes function is continuous at x iff its measure has no atom at x.