zibo yang (Jun 01 2021 at 15:50): zibo yang (Jun 01 2021 at 15:50):Hi. Is there any lemma in our probability library stating that "P(AB) = P(B)P(A|B)"?
Wenda Li (Jun 02 2021 at 02:41):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 ω)"
in src/HOL/Probability/Probability_Measure.thy.
Last updated: Dec 21 2024 at 16:20 UTC