`BookProof.InverseTransform.seedSet_total_measure` (hp : ∀ i, 0 ≤ p i) (hsum : cdf p n = 1) : ∑ k ∈ Finset.range n, volume (seedSet p k) = 1

Initializing...

`BookProof.InverseTransform.seedSet_total_measure` (hp : ∀ i, 0 ≤ p i) (hsum : cdf p n = 1) : ∑ k ∈ Finset.range n, volume (seedSet p k) = 1 · Prove2Me