src/HOL/Probability/Borel_Space.thy
changeset 56212 3253aaf73a01
parent 54775 2d3df8633dad
child 56371 fb9ae0727548
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -1111,7 +1111,7 @@
     1.4    assumes "\<And>i. f i \<in> borel_measurable M"
     1.5    shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
     1.6      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
     1.7 -  unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
     1.8 +  unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
     1.9  
    1.10  lemma sets_Collect_eventually_sequentially[measurable]:
    1.11    "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"