src/HOL/Probability/Independent_Family.thy
changeset 49795 9f2fb9b25a77
parent 49794 3c7b5988e094
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:30 2012 +0200
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Wed Oct 10 12:12:31 2012 +0200
     1.3 @@ -1170,4 +1170,12 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma (in prob_space) distributed_joint_indep:
     1.8 +  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
     1.9 +  assumes X: "distributed M S X Px" and Y: "distributed M T Y Py"
    1.10 +  assumes indep: "indep_var S X T Y"
    1.11 +  shows "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) (\<lambda>(x, y). Px x * Py y)"
    1.12 +  using indep_var_distribution_eq[of S X T Y] indep
    1.13 +  by (intro distributed_joint_indep'[OF S T X Y]) auto
    1.14 +
    1.15  end