Hi. Is there any lemma in our probability library stating that "P(AB) = P(B)P(A|B)"?
Not sure if the proposition is trivial given the definition of conditional probability:
definition "cond_prob M P Q = 𝒫(ω in M. P ω ∧ Q ω) / 𝒫(ω in M. Q ω)"
Last updated: Sep 25 2021 at 09:17 UTC