Stream: Beginner Questions

Topic: conditional


view this post on Zulip 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)"?

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC