`BookProof.ChapterDiffuseCdfModel.exists_cdf_eq` [IsProbabilityMeasure mu] [NullSingletonClass mu] {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) : ∃ x : ℝ, cdf mu x = t

Initializing...

`BookProof.ChapterDiffuseCdfModel.exists_cdf_eq` [IsProbabilityMeasure mu] [NullSingletonClass mu] {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) : ∃ x : ℝ, cdf mu x = t · Prove2Me