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)}"
```