Commit 2025-08-05 13:52 51cdf8c4
View on Github →feat: ProbabilityTheory.cdf_eq_real for measure on unitInterval (#27515)
Given a probability measure μ on I, the CDF of the pushforward of μ along Subtype.val is equal to the measure of the closed interval.