src/HOL/Limits.thy
changeset 51328 d63ec23c9125
parent 51022 78de6c7e8a58
child 51360 c4367ed99b5e
     1.1 --- a/src/HOL/Limits.thy	Mon Mar 04 09:57:54 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Wed Feb 20 12:04:42 2013 +0100
     1.3 @@ -264,6 +264,9 @@
     1.4  lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
     1.5    by (rule eventually_False [symmetric])
     1.6  
     1.7 +lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
     1.8 +  by (cases P) (simp_all add: eventually_False)
     1.9 +
    1.10  
    1.11  subsection {* Map function for filters *}
    1.12