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


I recently found the syntax of 𝒫 as

  "_prob" :: "pttrn ⇒ logic ⇒ logic ⇒ logic" ("('𝒫'((/_ in _./ _)'))")

  "𝒫(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.


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