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> {}"