src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44342 8321948340ea
parent 44286 8766839efb1b
child 44365 5daa55003649
equal deleted inserted replaced
44320:33439faadd67 44342:8321948340ea
   964   by (auto elim: eventually_rev_mp)
   964   by (auto elim: eventually_rev_mp)
   965 
   965 
   966 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   966 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
   967   unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
   967   unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
   968 
   968 
   969 lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
       
   970   unfolding trivial_limit_def ..
       
   971 
       
   972 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   969 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
   973   apply (safe elim!: trivial_limit_eventually)
   970   by (simp add: filter_eq_iff)
   974   apply (simp add: eventually_False [symmetric])
       
   975   done
       
   976 
   971 
   977 text{* Combining theorems for "eventually" *}
   972 text{* Combining theorems for "eventually" *}
   978 
   973 
   979 lemma eventually_rev_mono:
   974 lemma eventually_rev_mono:
   980   "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
   975   "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"