`BookProof.ChapterIrreversible.le_one_of_prob` (p : Fin n → ℝ) (hnn : ∀ a, 0 ≤ p a) (hsum : ∑ a, p a = 1) (a : Fin n) : p a ≤ 1

Initializing...

`BookProof.ChapterIrreversible.le_one_of_prob` (p : Fin n → ℝ) (hnn : ∀ a, 0 ≤ p a) (hsum : ∑ a, p a = 1) (a : Fin n) : p a ≤ 1 · Prove2Me