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 ω)"
```

in `src/HOL/Probability/Probability_Measure.thy`

.

Last updated: Sep 11 2024 at 16:22 UTC