`BookProof.ChapterE.stickBreaking_surjective` {N : ℕ} (P : Fin N → ℝ) (hP0 : ∀ n, 0 ≤ P n) (hPsum : ∑ n, P n = 1) : ∃ θ : Fin N → ℝ, ∀ n, stickBreaking θ n = P n

Initializing...

`BookProof.ChapterE.stickBreaking_surjective` {N : ℕ} (P : Fin N → ℝ) (hP0 : ∀ n, 0 ≤ P n) (hPsum : ∑ n, P n = 1) : ∃ θ : Fin N → ℝ, ∀ n, stickBreaking θ n = P n · Prove2Me