src/HOL/Analysis/Borel_Space.thy
changeset 64272 f76b6dda2e56
parent 64267 b9a1486e79be
child 64283 979cdfdf7a79
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -1348,7 +1348,7 @@
     1.4    shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
     1.5    using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
     1.6  
     1.7 -lemma borel_measurable_setprod[measurable (raw)]:
     1.8 +lemma borel_measurable_prod[measurable (raw)]:
     1.9    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
    1.10    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
    1.11    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
    1.12 @@ -1652,7 +1652,7 @@
    1.13    shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
    1.14    using assms by (induction S rule: infinite_finite_induct) auto
    1.15  
    1.16 -lemma borel_measurable_ereal_setprod[measurable (raw)]:
    1.17 +lemma borel_measurable_ereal_prod[measurable (raw)]:
    1.18    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
    1.19    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
    1.20    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
    1.21 @@ -1728,7 +1728,7 @@
    1.22    shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel"
    1.23    unfolding is_borel_def[symmetric] by transfer simp
    1.24  
    1.25 -lemma borel_measurable_setprod_ennreal[measurable (raw)]:
    1.26 +lemma borel_measurable_prod_ennreal[measurable (raw)]:
    1.27    fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal"
    1.28    assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
    1.29    shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"