`BookProof.ChapterDutchBook.Coherent.represents_singleton` {Pr : Finset Ω → ℝ} (h : Coherent Pr) (A : Finset Ω) : Pr A = ∑ ω ∈ A, Pr {ω}

Initializing...

`BookProof.ChapterDutchBook.Coherent.represents_singleton` {Pr : Finset Ω → ℝ} (h : Coherent Pr) (A : Finset Ω) : Pr A = ∑ ω ∈ A, Pr {ω} · Prove2Me