src/HOL/Probability/Measure_Space.thy
changeset 56154 f0a927235162
parent 54417 dbb8ecfe1337
child 56193 c726ecfb22b6
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -795,9 +795,9 @@
     1.4  
     1.5  lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
     1.6  proof -
     1.7 -  have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
     1.8 -    unfolding SUP_def image_compose
     1.9 -    unfolding surj_from_nat ..
    1.10 +  have "\<Union>range N = \<Union>(N ` range from_nat)" by simp
    1.11 +  then have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
    1.12 +    by (simp only: SUP_def image_comp)
    1.13    then show ?thesis by simp
    1.14  qed
    1.15