src/HOL/Probability/Caratheodory.thy
 changeset 52141 eff000cab70f parent 51329 4a3c453f99a1 child 55642 63beb38e9258
equal inserted replaced
52140:88a69da5d3fa 52141:eff000cab70f
`   705 lemma volume_finite_additive:`
`   705 lemma volume_finite_additive:`
`   706   assumes "volume M f" `
`   706   assumes "volume M f" `
`   707   assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"`
`   707   assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"`
`   708   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"`
`   708   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"`
`   709 proof -`
`   709 proof -`
`   710   have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"`
`   710   have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"`
`   711     using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)`
`   711     using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)`
`   712   with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"`
`   712   with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"`
`   713     unfolding volume_def by blast`
`   713     unfolding volume_def by blast`
`   714   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"`
`   714   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"`
`   715   proof (subst setsum_reindex_nonzero)`
`   715   proof (subst setsum_reindex_nonzero)`
`   716     fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"`
`   716     fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j"`
`   717     with `disjoint_family_on A I` have "A i = {}"`
`   717     with `disjoint_family_on A I` have "A i = {}"`