equal
deleted
inserted
replaced
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 = {}" |