--- 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))"
--- 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
--- 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
--- 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>
--- 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:
--- 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)"