src/HOL/Limits.thy
changeset 44571 bd91b77c4cd6
parent 44568 e6f291cb5810
child 44627 134c06282ae6
     1.1 --- a/src/HOL/Limits.thy	Sun Aug 28 16:28:07 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Aug 28 20:56:49 2011 -0700
     1.3 @@ -331,6 +331,9 @@
     1.4  apply (erule le_less_trans [OF dist_triangle])
     1.5  done
     1.6  
     1.7 +lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
     1.8 +  unfolding trivial_limit_def eventually_nhds by simp
     1.9 +
    1.10  lemma eventually_at_topological:
    1.11    "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    1.12  unfolding at_def eventually_within eventually_nhds by simp
    1.13 @@ -340,6 +343,13 @@
    1.14    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    1.15  unfolding at_def eventually_within eventually_nhds_metric by auto
    1.16  
    1.17 +lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
    1.18 +  unfolding trivial_limit_def eventually_at_topological
    1.19 +  by (safe, case_tac "S = {a}", simp, fast, fast)
    1.20 +
    1.21 +lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
    1.22 +  by (simp add: at_eq_bot_iff not_open_singleton)
    1.23 +
    1.24  
    1.25  subsection {* Boundedness *}
    1.26