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