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
```