--- a/src/HOL/Probability/Borel_Space.thy Fri Nov 16 18:49:46 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 16 18:45:57 2012 +0100
@@ -1114,21 +1114,10 @@
and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
-lemma sets_Collect_eventually_sequientially[measurable]:
+lemma sets_Collect_eventually_sequentially[measurable]:
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
unfolding eventually_sequentially by simp
-lemma convergent_ereal:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "convergent X \<longleftrightarrow> limsup X = liminf X"
- using ereal_Liminf_eq_Limsup_iff[of sequentially]
- by (auto simp: convergent_def)
-
-lemma convergent_ereal_limsup:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "convergent X \<Longrightarrow> limsup X = lim X"
- by (auto simp: convergent_def limI lim_imp_Limsup)
-
lemma sets_Collect_ereal_convergent[measurable]:
fixes f :: "nat \<Rightarrow> 'a => ereal"
assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"