src/HOL/Probability/Finite_Product_Measure.thy

 
 abbreviation
   "Pi\<^sub>M I M \<equiv> PiM I M"
 
 syntax
-  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIM _:_./ _)" 10)
-syntax (xsymbols)
   "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
 translations
-  "PIM x:I. M" == "CONST PiM I (%x. M)"
+  "\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
 
 lemma extend_measure_cong:
   assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
   shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
   unfolding extend_measure_def by (auto simp add: assms)

   assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
   using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
 
 lemma sets_PiM_I:
   assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
-  shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
+  shows "prod_emb I M J (PIE j:J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
 proof cases
   assume "J = {}"
   then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
     by (auto simp: prod_emb_def)
   then show ?thesis

     using A f by (auto intro!: measurable_sets)
 qed fact
 
 lemma sets_PiM_I_finite[measurable]:
   assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
-  shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
+  shows "(PIE j:I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
   using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
 
 lemma measurable_component_singleton[measurable (raw)]:
   assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
 proof (unfold measurable_def, intro CollectI conjI ballI)