src/HOL/Limits.thy
changeset 45031 9583f2b56f85
parent 44627 134c06282ae6
child 45294 3c5d3d286055
     1.1 --- a/src/HOL/Limits.thy	Tue Sep 20 15:23:17 2011 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Sep 20 10:52:08 2011 -0700
     1.3 @@ -298,7 +298,10 @@
     1.4    by (rule eventually_Abs_filter, rule is_filter.intro)
     1.5       (auto elim!: eventually_rev_mp)
     1.6  
     1.7 -lemma within_UNIV: "F within UNIV = F"
     1.8 +lemma within_UNIV [simp]: "F within UNIV = F"
     1.9 +  unfolding filter_eq_iff eventually_within by simp
    1.10 +
    1.11 +lemma within_empty [simp]: "F within {} = bot"
    1.12    unfolding filter_eq_iff eventually_within by simp
    1.13  
    1.14  lemma eventually_nhds:
    1.15 @@ -584,6 +587,9 @@
    1.16  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
    1.17    by (simp only: tendsto_iff Zfun_def dist_norm)
    1.18  
    1.19 +lemma tendsto_bot [simp]: "(f ---> a) bot"
    1.20 +  unfolding tendsto_def by simp
    1.21 +
    1.22  lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
    1.23    unfolding tendsto_def eventually_at_topological by auto
    1.24