src/HOL/Probability/Stopping_Time.thy
changeset 69313 b021008c5397
parent 67226 ec32cdaab97b
     1.1 --- a/src/HOL/Probability/Stopping_Time.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -87,9 +87,9 @@
     1.4    fix AA :: "nat \<Rightarrow> 'a set" and t assume "range AA \<subseteq> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
     1.5    then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
     1.6      by auto
     1.7 -  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
     1.8 +  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t}"
     1.9      by auto
    1.10 -  finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
    1.11 +  finally show "{\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t} \<in> sets (F t)" .
    1.12  qed auto
    1.13  
    1.14  lemma sets_pre_sigma: "stopping_time F T \<Longrightarrow> sets (pre_sigma T) = {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"