src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44342 8321948340ea
parent 44286 8766839efb1b
child 44365 5daa55003649
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Aug 20 06:34:51 2011 -0700
@@ -966,13 +966,8 @@
 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
 
-lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
-  unfolding trivial_limit_def ..
-
 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
-  apply (safe elim!: trivial_limit_eventually)
-  apply (simp add: eventually_False [symmetric])
-  done
+  by (simp add: filter_eq_iff)
 
 text{* Combining theorems for "eventually" *}