`BookProof.ChapterBayesInference.posterior_nonneg` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) (x : X) : 0 ≤ posterior prior L y x

Initializing...

`BookProof.ChapterBayesInference.posterior_nonneg` (hprior : ∀ x, 0 ≤ prior x) (hL : ∀ x y, 0 ≤ L x y) (y : Y) (x : X) : 0 ≤ posterior prior L y x · Prove2Me