src/HOL/Lim.thy
 changeset 44205 18da2a87421c parent 44194 0639898074ae child 44217 5cdad94bdc29
```--- a/src/HOL/Lim.thy	Sun Aug 14 08:45:38 2011 -0700
+++ b/src/HOL/Lim.thy	Sun Aug 14 10:25:43 2011 -0700
@@ -181,32 +181,32 @@
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
by (rule tendsto_rabs_zero_iff)

-lemma at_neq_bot:
+lemma trivial_limit_at:
fixes a :: "'a::real_normed_algebra_1"
-  shows "at a \<noteq> bot"  -- {* TODO: find a more appropriate class *}
-unfolding eventually_False [symmetric]
+  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
+unfolding trivial_limit_def
unfolding eventually_at dist_norm
by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)

lemma LIM_const_not_eq:
fixes a :: "'a::real_normed_algebra_1"
-  fixes k L :: "'b::metric_space"
+  fixes k L :: "'b::t2_space"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"

lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]

lemma LIM_const_eq:
fixes a :: "'a::real_normed_algebra_1"
-  fixes k L :: "'b::metric_space"
+  fixes k L :: "'b::t2_space"
shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"