src/HOL/Probability/Caratheodory.thy
changeset 52141 eff000cab70f
parent 51329 4a3c453f99a1
child 55642 63beb38e9258
equal deleted 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 = {}"