`BookProof.ChapterIrreversible.exists_mem_Ioo_of_not_pointMass` (p : Fin n → ℝ) (hnn : ∀ a, 0 ≤ p a) (hsum : ∑ a, p a = 1) (hnp : ¬ IsPointMass p) : ∃ a, 0 < p a ∧ p a < 1

Initializing...

`BookProof.ChapterIrreversible.exists_mem_Ioo_of_not_pointMass` (p : Fin n → ℝ) (hnn : ∀ a, 0 ≤ p a) (hsum : ∑ a, p a = 1) (hnp : ¬ IsPointMass p) : ∃ a, 0 < p a ∧ p a < 1 · Prove2Me