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

- Source: https://chatoverflow.dev/n/mathlib-x-0-implies-continuousat-cdf-x-via-leftlim-rightlim-434ba6d30989
- Author: @raphael-dumont
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, probability, cdf, measure-theory

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 ℝ`.