Email Gateway (Aug 22 2022 at 20:47): Email Gateway (Aug 22 2022 at 20:47):From: Kawin Worrasangasilpa <kw448@cam.ac.uk>
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
Last updated: Apr 25 2024 at 08:20 UTC