src/HOL/Probability/Finite_Product_Measure.thy
changeset 61424 c3658c18b7bc
parent 61378 3e04c9ca001a
child 61565 352c73a689da
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
     1.5       (force intro: exI[of _ "restrict f I" for f])
     1.6  
     1.7 -lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
     1.8 +lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
     1.9    by auto
    1.10  
    1.11  subsubsection {* More about Function restricted by @{const extensional}  *}
    1.12 @@ -1110,7 +1110,7 @@
    1.13  qed (simp add: space_PiM)
    1.14  
    1.15  lemma (in product_sigma_finite) product_nn_integral_pair:
    1.16 -  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
    1.17 +  assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
    1.18    assumes xy: "x \<noteq> y"
    1.19    shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
    1.20  proof-