equal
deleted
inserted
replaced
638 by (rule order_antisym) |
638 by (rule order_antisym) |
639 qed |
639 qed |
640 |
640 |
641 lemma measure_down: |
641 lemma measure_down: |
642 "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
642 "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" |
643 by (simp add: measure_space_def positive_def countably_additive_def) |
643 by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq) |
644 blast |
|
645 |
644 |
646 subsection {* Caratheodory's theorem *} |
645 subsection {* Caratheodory's theorem *} |
647 |
646 |
648 theorem (in ring_of_sets) caratheodory': |
647 theorem (in ring_of_sets) caratheodory': |
649 assumes posf: "positive M f" and ca: "countably_additive M f" |
648 assumes posf: "positive M f" and ca: "countably_additive M f" |