Measurable on euclidean space is equiv. to measurable components
--- a/src/HOL/Probability/Borel.thy Fri Aug 27 13:48:10 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Fri Aug 27 14:05:03 2010 +0200
@@ -658,6 +658,30 @@
"(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
using borel_measurable_iff_halfspace_greater[where 'c=real] by simp
+lemma borel_measureable_euclidean_component:
+ "(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel_space"
+ unfolding borel_space_def[where 'a=real]
+proof (rule borel_space.measurable_sigma)
+ fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def .
+ from open_vimage_euclidean_component[OF this]
+ show "(\<lambda>x. x $$ i) -` S \<inter> space borel_space \<in> sets borel_space"
+ by (auto intro: borel_space_open)
+qed auto
+
+lemma (in sigma_algebra) borel_measureable_euclidean_space:
+ fixes f :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+ shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M)"
+proof safe
+ fix i assume "f \<in> borel_measurable M"
+ then show "(\<lambda>x. f x $$ i) \<in> borel_measurable M"
+ using measurable_comp[of f _ _ "\<lambda>x. x $$ i", unfolded comp_def]
+ by (auto intro: borel_measureable_euclidean_component)
+next
+ assume f: "\<forall>i<DIM('c). (\<lambda>x. f x $$ i) \<in> borel_measurable M"
+ then show "f \<in> borel_measurable M"
+ unfolding borel_measurable_iff_halfspace_le by auto
+qed
+
subsection "Borel measurable operators"
lemma (in sigma_algebra) affine_borel_measurable_vector: