equal
deleted
inserted
replaced
938 using sigma_finite by auto |
938 using sigma_finite by auto |
939 then show ?thesis |
939 then show ?thesis |
940 proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI) |
940 proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI) |
941 from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto |
941 from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto |
942 then show "(\<Union>n. \<Union> i\<le>n. F i) = space M" |
942 then show "(\<Union>n. \<Union> i\<le>n. F i) = space M" |
943 using F by fastsimp |
943 using F by fastforce |
944 next |
944 next |
945 fix n |
945 fix n |
946 have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F |
946 have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F |
947 by (auto intro!: measure_finitely_subadditive) |
947 by (auto intro!: measure_finitely_subadditive) |
948 also have "\<dots> < \<infinity>" |
948 also have "\<dots> < \<infinity>" |