src/HOL/Probability/Borel_Space.thy
changeset 50104 de19856feb54
parent 50096 7c9c5b1b6cd7
child 50244 de72bbe42190
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:49:46 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     1.3 @@ -1114,21 +1114,10 @@
     1.4      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
     1.5    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
     1.6  
     1.7 -lemma sets_Collect_eventually_sequientially[measurable]:
     1.8 +lemma sets_Collect_eventually_sequentially[measurable]:
     1.9    "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
    1.10    unfolding eventually_sequentially by simp
    1.11  
    1.12 -lemma convergent_ereal:
    1.13 -  fixes X :: "nat \<Rightarrow> ereal"
    1.14 -  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
    1.15 -  using ereal_Liminf_eq_Limsup_iff[of sequentially]
    1.16 -  by (auto simp: convergent_def)
    1.17 -
    1.18 -lemma convergent_ereal_limsup:
    1.19 -  fixes X :: "nat \<Rightarrow> ereal"
    1.20 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
    1.21 -  by (auto simp: convergent_def limI lim_imp_Limsup)
    1.22 -
    1.23  lemma sets_Collect_ereal_convergent[measurable]: 
    1.24    fixes f :: "nat \<Rightarrow> 'a => ereal"
    1.25    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"