src/HOL/Probability/Fin_Map.thy
changeset 61988 34b51f436e92
parent 61973 0c7e865fa7cb
child 62101 26c0a70f78a3
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Wed Dec 30 18:47:13 2015 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Wed Dec 30 19:41:48 2015 +0100
     1.3 @@ -101,11 +101,9 @@
     1.4    "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
     1.5  
     1.6  syntax
     1.7 -  "_Pi'"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI' _:_./ _)" 10)
     1.8 -syntax (xsymbols)
     1.9    "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>' _\<in>_./ _)"   10)
    1.10  translations
    1.11 -  "PI' x:A. B" == "CONST Pi' A (%x. B)"
    1.12 +  "\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"
    1.13  
    1.14  subsubsection\<open>Basic Properties of @{term Pi'}\<close>
    1.15  
    1.16 @@ -610,11 +608,9 @@
    1.17    "Pi\<^sub>F I M \<equiv> PiF I M"
    1.18  
    1.19  syntax
    1.20 -  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIF _:_./ _)" 10)
    1.21 -syntax (xsymbols)
    1.22    "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>F _\<in>_./ _)"  10)
    1.23  translations
    1.24 -  "PIF x:I. M" == "CONST PiF I (%x. M)"
    1.25 +  "\<Pi>\<^sub>F x\<in>I. M" == "CONST PiF I (%x. M)"
    1.26  
    1.27  lemma PiF_gen_subset: "{(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))} \<subseteq>
    1.28      Pow (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j)))"
    1.29 @@ -1094,7 +1090,7 @@
    1.30    qed
    1.31  qed
    1.32  
    1.33 -lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. PI' j : J. UNIV) = UNIV" by auto
    1.34 +lemma finmap_UNIV[simp]: "(\<Union>J\<in>Collect finite. \<Pi>' j\<in>J. UNIV) = UNIV" by auto
    1.35  
    1.36  lemma borel_eq_PiF_borel:
    1.37    shows "(borel :: ('i::countable \<Rightarrow>\<^sub>F 'a::polish_space) measure) =