src/HOL/Probability/Infinite_Product_Measure.thy
changeset 49784 5e5b2da42a69
parent 49780 92a58f80b20c
child 49804 ace9b5a83e60
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Oct 10 12:12:23 2012 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4    let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
     1.5    show "Int_stable ?J"
     1.6      by (rule Int_stable_PiE)
     1.7 -  show "range ?F \<subseteq> ?J" "incseq ?F" "(\<Union>i. ?F i) = ?\<Omega>"
     1.8 +  show "range ?F \<subseteq> ?J" "(\<Union>i. ?F i) = ?\<Omega>"
     1.9      using `finite J` by (auto intro!: prod_algebraI_finite)
    1.10    { fix i show "emeasure ?P (?F i) \<noteq> \<infinity>" by simp }
    1.11    show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)