src/HOL/Analysis/Measure_Space.thy
changeset 67673 c8caefb20564
parent 67399 eab6ce8368fa
child 67962 0acdcd8f4ba1
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Feb 18 20:08:21 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Mon Feb 19 16:44:45 2018 +0000
     1.3 @@ -1749,6 +1749,10 @@
     1.4  lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
     1.5    using fmeasurableI2[of A M "A - B"] by auto
     1.6  
     1.7 +lemma fmeasurable_Int_fmeasurable:
     1.8 +   "\<lbrakk>S \<in> fmeasurable M; T \<in> sets M\<rbrakk> \<Longrightarrow> (S \<inter> T) \<in> fmeasurable M"
     1.9 +  by (meson fmeasurableD fmeasurableI2 inf_le1 sets.Int)
    1.10 +
    1.11  lemma fmeasurable_UN:
    1.12    assumes "countable I" "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> A" "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M" "A \<in> fmeasurable M"
    1.13    shows "(\<Union>i\<in>I. F i) \<in> fmeasurable M"