# [isabelle] Probability P(x in M, Q) usage

Hi,
I recently found the syntax of 𝒫 as
syntax
"_prob" :: "pttrn ⇒ logic ⇒ logic ⇒ logic" ("('𝒫'((/_ in _./ _)'))")
translations
"𝒫(x in M. P)" => "CONST measure M {x ∈ CONST space M. P}"
but I could not find any well-known rules related to it (e.g.
inclusion-exclusion:[image: {\mathbb {P}}(A_{1}\cup A_{2})={\mathbb
{P}}(A_{1})+{\mathbb {P}}(A_{2})-{\mathbb {P}}(A_{1}\cap A_{2}),]), so I
would like to know if anything of that kind has been formalised or we
always need to go down to the translation form of 𝒫 ( "CONST measure M {x
∈ CONST space M. P}" ) and deal with it by using 'measure' function, hence
always proving in the set level, when it comes to proof.
Thanks,
Kawin

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*