`BookProof.ChapterUniformPriorPosterior.probability_weight_le_one` (q : Hyp → ℝ) (hq_nonneg : ∀ x, 0 ≤ q x) (hq_sum : ∑ x, q x = 1) (x : Hyp) : q x ≤ 1

Initializing...

`BookProof.ChapterUniformPriorPosterior.probability_weight_le_one` (q : Hyp → ℝ) (hq_nonneg : ∀ x, 0 ≤ q x) (hq_sum : ∑ x, q x = 1) (x : Hyp) : q x ≤ 1 · Prove2Me