# HG changeset patch
# User wenzelm
# Date 1484648781 -3600
# Node ID 6108dddad9f0f2710dc545013e06165940c3c55e
# Parent  8007f10195af4affa947b33d7c194ee447753af4
more symbols via abbrevs;

diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -8,7 +8,7 @@
 imports Binary_Product_Measure
 begin
 
-lemma PiE_choice: "(\<exists>f\<in>PiE I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
+lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
   by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
      (force intro: exI[of _ "restrict f I" for f])
 
@@ -61,7 +61,7 @@
 
 lemma PiE_cancel_merge[simp]:
   "I \<inter> J = {} \<Longrightarrow>
-    merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
+    merge I J (x, y) \<in> Pi\<^sub>E (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
   by (auto simp: PiE_def restrict_Pi_cancel)
 
 lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
@@ -114,7 +114,7 @@
 subsubsection \<open>Products\<close>
 
 definition prod_emb where
-  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
+  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
 
 lemma prod_emb_iff:
   "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
@@ -216,7 +216,7 @@
 proof (intro iffI set_eqI)
   fix A assume "A \<in> ?L"
   then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
-    and A: "A = prod_emb I M J (PIE j:J. E j)"
+    and A: "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
     by (auto simp: prod_algebra_def)
   let ?A = "\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i)"
   have A: "A = ?A"
@@ -234,7 +234,7 @@
 
 lemma prod_algebraI:
   "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
-    \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
+    \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M"
   by (auto simp: prod_algebra_def)
 
 lemma prod_algebraI_finite:
@@ -250,7 +250,7 @@
 
 lemma prod_algebraE:
   assumes A: "A \<in> prod_algebra I M"
-  obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
+  obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
     "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
   using A by (auto simp: prod_algebra_def)
 
@@ -459,9 +459,9 @@
         by (auto simp: PiE_def Pi_def)
       then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
         by metis
-      with \<open>x i \<in> A\<close> have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
+      with \<open>x i \<in> A\<close> have "\<exists>n\<in>Pi\<^sub>E (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
         by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
-    then have "Z = (\<Union>n\<in>PiE (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
+    then have "Z = (\<Union>n\<in>Pi\<^sub>E (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
       unfolding Z_def
       by (auto simp add: set_eq_iff ball_conj_distrib \<open>i\<in>j\<close> A'_i dest: bspec[OF _ \<open>i\<in>j\<close>]
                cong: conj_cong)
@@ -509,10 +509,10 @@
 
 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 (\<Pi>\<^sub>M i\<in>I. M i)"
+  shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>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))"
+  then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))"
     by (auto simp: prod_emb_def)
   then show ?thesis
     by (auto simp add: sets_PiM intro!: sigma_sets_top)
@@ -576,7 +576,7 @@
 
 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 (\<Pi>\<^sub>M i\<in>I. M i)"
+  shows "(\<Pi>\<^sub>E j\<in>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)]:
@@ -741,7 +741,7 @@
   assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)"
 proof cases
   assume "I \<noteq> {}"
-  then have "PiE I E = (\<Inter>i\<in>I. prod_emb I M {i} (PiE {i} E))"
+  then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
     using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
   also have "\<dots> \<in> sets (PiM I M)"
     using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
@@ -793,7 +793,7 @@
   show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
     unfolding space_PiM[symmetric] by fact+
   fix X assume "X \<in> prod_algebra I M"
-  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
+  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
     and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
     by (force elim!: prod_algebraE)
   then show "emeasure P X = emeasure Q X"
@@ -822,7 +822,7 @@
     by (auto simp: space_PiM)
 next
   fix X assume X: "X \<in> prod_algebra I M"
-  then obtain J E where X: "X = prod_emb I M J (PIE j:J. E j)"
+  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
     and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
     by (force elim!: prod_algebraE)
   then show "emeasure P X = emeasure Q X"
@@ -976,10 +976,10 @@
     "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
     in_space: "\<And>j. space (M j) = (\<Union>F j)"
     using sigma_finite_countable by (metis subset_eq)
-  moreover have "(\<Union>(PiE I ` PiE I F)) = space (Pi\<^sub>M I M)"
+  moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
     using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
   ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
-    by (intro exI[of _ "PiE I ` PiE I F"])
+    by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
        (auto intro!: countable_PiE sets_PiM_I_finite
              simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
 qed
@@ -1003,7 +1003,7 @@
   interpret I: finite_product_sigma_finite M I by standard fact
   interpret J: finite_product_sigma_finite M J by standard fact
   fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
-  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = PiE I A \<times> PiE J A"
+  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = Pi\<^sub>E I A \<times> Pi\<^sub>E J A"
     using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
   from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
       (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -17,7 +17,7 @@
 to each factor is continuous.
 
 To form a product of objects in Isabelle/HOL, all these objects should be subsets of a common type
-'a. The product is then @{term "PiE I X"}, the set of elements from 'i to 'a such that the $i$-th
+'a. The product is then @{term "Pi\<^sub>E I X"}, the set of elements from 'i to 'a such that the $i$-th
 coordinate belongs to $X\;i$ for all $i \in I$.
 
 Hence, to form a product of topological spaces, all these spaces should be subsets of a common type.
@@ -696,7 +696,7 @@
 lemma product_topology_countable_basis:
   shows "\<exists>K::(('a::countable \<Rightarrow> 'b::second_countable_topology) set set).
           topological_basis K \<and> countable K \<and>
-          (\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
+          (\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV})"
 proof -
   obtain B::"'b set set" where B: "countable B \<and> topological_basis B"
     using ex_countable_basis by auto
@@ -708,7 +708,7 @@
     using that unfolding B2_def using B topological_basis_open by auto
 
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
-  have i: "\<forall>k\<in>K. \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+  have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
 
   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
@@ -1335,11 +1335,11 @@
   "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
 proof
   obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
-            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = PiE UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
+            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
     using product_topology_countable_basis by fast
   have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
   proof -
-    obtain X where H: "k = PiE UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
       using K(3)[OF `k \<in> K`] by blast
     show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
   qed
diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -2539,7 +2539,7 @@
   let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
                     cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
                          (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
-  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
+  let ?D0 = "?K0 ` (SIGMA n:UNIV. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^n)))"
   obtain \<D>0 where count: "countable \<D>0"
              and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
              and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
@@ -2698,7 +2698,7 @@
     proof (rule finite_subset)
       let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
                                         (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
-                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
+                ` (SIGMA m:atMost n. Pi\<^sub>E Basis (\<lambda>i::'a. lessThan (2^m)))"
       have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
       proof -
         have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -89,7 +89,7 @@
   done
 
 lemma countable_PiE:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
+  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
 
 lemma continuous_on_cases:
@@ -2173,7 +2173,7 @@
 
 lemma interior_complement: "interior (- S) = - closure S"
   by (simp add: closure_interior)
-   
+
 lemma interior_diff: "interior(S - T) = interior S - closure T"
   by (simp add: Diff_eq interior_complement)
 
@@ -5348,7 +5348,7 @@
   show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using l r by fast
 qed
-  
+
 subsubsection \<open>Intersecting chains of compact sets\<close>
 
 proposition bounded_closed_chain:
@@ -10727,8 +10727,8 @@
   qed
   from X0(1,2) this show ?thesis ..
 qed
-  
-  
+
+
 subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 
 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -5,7 +5,9 @@
 section \<open>Pi and Function Sets\<close>
 
 theory FuncSet
-imports Hilbert_Choice Main
+  imports Hilbert_Choice Main
+  abbrevs PiE = "Pi\<^sub>E"
+    PIE = "\<Pi>\<^sub>E"
 begin
 
 definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
@@ -360,10 +362,10 @@
 lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
   by (simp add: PiE_def)
 
-lemma PiE_empty_domain[simp]: "PiE {} T = {\<lambda>x. undefined}"
+lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}"
   unfolding PiE_def by simp
 
-lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
+lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
   unfolding PiE_def by simp
 
 lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
@@ -386,29 +388,29 @@
   qed
 qed (auto simp: PiE_def)
 
-lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
+lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
   unfolding PiE_def by auto (auto dest!: extensional_arb)
 
-lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
+lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
   unfolding PiE_def by auto
 
-lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
+lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T"
   unfolding PiE_def extensional_def by auto
 
-lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
+lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T"
   unfolding PiE_def extensional_def by auto
 
-lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
 proof -
   {
-    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
-    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S"
+    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
       by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   }
   moreover
   {
-    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
-    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S"
+    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
       by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
   }
   ultimately show ?thesis
@@ -422,25 +424,25 @@
   unfolding PiE_def by (auto simp: Pi_cong)
 
 lemma PiE_E [elim]:
-  assumes "f \<in> PiE A B"
+  assumes "f \<in> Pi\<^sub>E A B"
   obtains "x \<in> A" and "f x \<in> B x"
     | "x \<notin> A" and "f x = undefined"
   using assms by (auto simp: Pi_def PiE_def extensional_def)
 
 lemma PiE_I[intro!]:
-  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
+  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B"
   by (simp add: PiE_def extensional_def)
 
-lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
+lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C"
   by auto
 
-lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
+lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
   by (simp add: PiE_def Pi_iff)
 
-lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
+lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
   by (simp add: extensional_restrict PiE_def)
 
-lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
+lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S"
   by (auto simp: PiE_iff)
 
 lemma PiE_eq_subset:
diff -r 8007f10195af -r 6108dddad9f0 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Jan 16 21:53:44 2017 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jan 17 11:26:21 2017 +0100
@@ -14,7 +14,7 @@
 proof (rule PiM_eqI)
   fix X assume X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
   { fix J X assume J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" and X: "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
-    have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
+    have "emeasure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod>i\<in>J. M i (X i))"
     proof (subst emeasure_extend_measure_Pair[OF PiM_def, where \<mu>'=lim], goal_cases)
       case 1 then show ?case
         by (simp add: M.emeasure_space_1 emeasure_PiM Pi_iff sets_PiM_I_finite emeasure_lim_emb)
@@ -28,7 +28,7 @@
       add: M.emeasure_space_1 sets_lim[symmetric] emeasure_countably_additive emeasure_positive) }
   note * = this
 
-  have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
+  have "emeasure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod>i\<in>J. M i (X i))"
   proof (cases "J \<noteq> {} \<or> I = {}")
     case False
     then obtain i where i: "J = {}" "i \<in> I" by auto
@@ -340,8 +340,8 @@
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
     using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (S \<Otimes>\<^sub>M S) =
-    (prod_emb ?I ?M (J \<inter> {..<i}) (PIE j:J \<inter> {..<i}. E j)) \<times>
-    (prod_emb ?I ?M ((op + i) -` J) (PIE j:(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
+    (prod_emb ?I ?M (J \<inter> {..<i}) (\<Pi>\<^sub>E j\<in>J \<inter> {..<i}. E j)) \<times>
+    (prod_emb ?I ?M ((op + i) -` J) (\<Pi>\<^sub>E j\<in>(op + i) -` J. E (i + j)))" (is "_ = ?E \<times> ?F")
    by (auto simp: space_pair_measure space_PiM prod_emb_def all_conj_distrib PiE_iff
                split: split_comb_seq split_comb_seq_asm)
   then have "emeasure ?D ?X = emeasure (S \<Otimes>\<^sub>M S) (?E \<times> ?F)"
@@ -368,11 +368,11 @@
   let "distr _ _ ?f" = "?D"
 
   fix J E assume J: "finite J" "J \<subseteq> ?I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets M"
-  let ?X = "prod_emb ?I ?M J (PIE j:J. E j)"
+  let ?X = "prod_emb ?I ?M J (\<Pi>\<^sub>E j\<in>J. E j)"
   have "\<And>j x. j \<in> J \<Longrightarrow> x \<in> E j \<Longrightarrow> x \<in> space M"
     using J(3)[THEN sets.sets_into_space] by (auto simp: space_PiM Pi_iff subset_eq)
   with J have "?f -` ?X \<inter> space (M \<Otimes>\<^sub>M S) = (if 0 \<in> J then E 0 else space M) \<times>
-    (prod_emb ?I ?M (Suc -` J) (PIE j:Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
+    (prod_emb ?I ?M (Suc -` J) (\<Pi>\<^sub>E j\<in>Suc -` J. E (Suc j)))" (is "_ = ?E \<times> ?F")
    by (auto simp: space_pair_measure space_PiM PiE_iff prod_emb_def all_conj_distrib
       split: nat.split nat.split_asm)
   then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^sub>M S) (?E \<times> ?F)"