ContinuousCDF.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.continuous_stieltjesFunction_of_nullSingletonClass line 13
Source documentation
A Stieltjes function has no jumps when its associated measure has no point atoms.
```
theorem continuous_stieltjesFunction_of_nullSingletonClass
    (f : StieltjesFunction ℝ) [NullSingletonClass f.measure] : Continuous f := by
…
```
theorem OAI.Problem356.continuous_cdf_of_nullSingletonClass line 26
Source documentation
The cumulative distribution function of an atomless real probability measure is continuous.
```
theorem continuous_cdf_of_nullSingletonClass (mu : Measure ℝ)
    [IsProbabilityMeasure mu] [NullSingletonClass mu] :
    Continuous (ProbabilityTheory.cdf mu) := by
…
```