Theorem ProbabilityTheory.unitInterval.cdf_eq_real

Modification history

2025-08-05 13:52
Mathlib/Probability/CDF.lean
feat: `ProbabilityTheory.cdf_eq_real` for measure on `unitInterval` (#27515) …
Added ProbabilityTheory.unitInterval.cdf_eq_realView on Github →