summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 = {}" |