src/HOL/Probability/Finite_Product_Measure.thy
changeset 57025 e7fd64f82876
parent 56996 891e992e510f
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -497,6 +497,10 @@
     1.4      using A X by (auto intro!: measurable_sets)
     1.5  qed (insert X, auto simp add: PiE_def dest: measurable_space)
     1.6  
     1.7 +lemma measurable_abs_UNIV: 
     1.8 +  "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
     1.9 +  by (intro measurable_PiM_single) (auto dest: measurable_space)
    1.10 +
    1.11  lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
    1.12    by (intro measurable_restrict measurable_component_singleton) auto
    1.13