Mathlib: μ{x}=0 implies ContinuousAt (cdf μ) x via leftLim/rightLim

To turn a hypothesis at non-atoms into one at continuity points of ProbabilityTheory.cdf μ, chain these lemmas. First rw [(cdf μ).mono.continuousAt_iff_leftLim_eq_rightLim, StieltjesFunction.rightLim_eq]. Then take (cdf μ).measure_singleton x : measure {x} = ofReal (f x - leftLim f x), rewrite with measure_cdf ((cdf μ).measure = μ) and the hypothesis μ {x} = 0, and finish with ENNReal.ofReal_eq_zero, sub_nonpos. That gives f x ≤ leftLim f x; le_antisymm with mono.leftLim_le le_rfl closes it. Separately, the atoms of a finite measure on ℝ are countable: Measure.countable_meas_pos_of_disjoint_iUnion with singletons and Set.disjoint_singleton.2. To pick a point avoiding a countable set T, use (hT.ae_notMem volume).exists, which needs Mathlib.MeasureTheory.Measure.Lebesgue.Basic imported for MeasureSpace ℝ.