summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Independent_Family.thy

changeset 44282 | f0de18b62d63 |

parent 43920 | cedb5cb948fd |

child 45777 | c36637603821 |

1.1 --- a/src/HOL/Probability/Independent_Family.thy Thu Aug 18 17:42:35 2011 +0200 1.2 +++ b/src/HOL/Probability/Independent_Family.thy Thu Aug 18 13:36:58 2011 -0700 1.3 @@ -563,7 +563,7 @@ 1.4 with F have "(\<lambda>i. prob X * prob (F i)) sums prob (X \<inter> (\<Union>i. F i))" 1.5 by simp 1.6 moreover have "(\<lambda>i. prob X * prob (F i)) sums (prob X * prob (\<Union>i. F i))" 1.7 - by (intro mult_right.sums finite_measure_UNION F dis) 1.8 + by (intro sums_mult finite_measure_UNION F dis) 1.9 ultimately have "prob (X \<inter> (\<Union>i. F i)) = prob X * prob (\<Union>i. F i)" 1.10 by (auto dest!: sums_unique) 1.11 with F show "(\<Union>i. F i) \<in> sets ?D"