src/HOL/Probability/Independent_Family.thy
changeset 50021 d96a3f468203
parent 50003 8c213922ed49
child 50087 635d73673b5e
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Nov 06 15:15:33 2012 +0100
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Nov 06 19:18:35 2012 +0100
     1.3 @@ -1004,9 +1004,6 @@
     1.4    "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
     1.5    using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
     1.6  
     1.7 -lemma measurable_id_prod[measurable (raw)]: "i = j \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)"
     1.8 -  by simp
     1.9 -
    1.10  lemma (in product_sigma_finite) distr_component:
    1.11    "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
    1.12  proof (intro measure_eqI[symmetric])