src/HOL/Probability/Lebesgue_Measure.thy
 changeset 50123 69b35a75caf3 parent 50105 65d5b18e1626 child 50244 de72bbe42190
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 16:14:18 2012 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 19 12:29:02 2012 +0100
1.3 @@ -935,7 +935,7 @@
1.4    fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
1.5    then obtain x where  "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
1.6    then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
1.7 -    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
1.8 +    using DIM_positive by (auto simp add: set_eq_iff e2p_def
1.9        euclidean_eq[where 'a='a] eucl_less[where 'a='a])
1.10    then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
1.11  qed (auto simp: e2p_def)
1.12 @@ -953,7 +953,7 @@
1.13    let ?A = "{w \<in> space ?P. (p2e w :: 'a) \$\$ i \<le> x}"
1.14    assume "i < DIM('a)"
1.15    then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
1.16 -    using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
1.17 +    using DIM_positive by (auto simp: space_PiM p2e_def PiE_def split: split_if_asm)
1.18    then show "?A \<in> sets ?P"
1.19      by auto
1.20  qed
1.21 @@ -966,7 +966,7 @@
1.22    let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
1.23    fix a b :: 'a
1.24    have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a \$\$ i .. b \$\$ i})"
1.25 -    by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
1.26 +    by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff)
1.27    have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
1.28    proof cases
1.29      assume "{a..b} \<noteq> {}"
```