# Re: [isabelle] looking for some measure.union_inter theorem

Am Dienstag, den 06.11.2012, 00:46 +0100 schrieb Henri DEBRAT:
> Hi all,
>
>
> I am trying to demonstrate the following probability lemma (prob being defined as a measure in a prob_space according to the Probability library) :
> "⋀ A B. finite A ⟹ finite B ⟹ prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
>
> The closer theorem I could discover in the Isabelle/HOL library is Finite_Set.folding_image_simple.union_inter.
> [..]
As Stephan Merz already mentioned this is better done with
finite_measure_Union and finite_measure_Diff in the prob_space locale.
fold_image (op +) is used to define setsum and setprod, so it is easier
to just use setsum. The rules you need are setsum_Un_Int and
measure_eq_setsum_singleton. But my experience is, that staying as long
as possible in the probability theory setting (i.e. use prob on sets) is
usually easier.
I hope this helps,
Johannes

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