`BookProof.ChapterDutchBook.Coherent.univ` [Fintype Ω] {Pr : Finset Ω → ℝ} (h : Coherent Pr) : Pr (Finset.univ : Finset Ω) = 1

Initializing...

`BookProof.ChapterDutchBook.Coherent.univ` [Fintype Ω] {Pr : Finset Ω → ℝ} (h : Coherent Pr) : Pr (Finset.univ : Finset Ω) = 1 · Prove2Me