src/HOL/Lim.thy
 changeset 31392 69570155ddf8 parent 31355 3d18766ddc4b child 31487 93938cafc0e6
```     1.1 --- a/src/HOL/Lim.thy	Tue Jun 02 15:37:59 2009 -0700
1.2 +++ b/src/HOL/Lim.thy	Tue Jun 02 17:03:22 2009 -0700
1.3 @@ -13,10 +13,6 @@
1.4  text{*Standard Definitions*}
1.5
1.6  definition
1.7 -  at :: "'a::metric_space \<Rightarrow> 'a filter" where
1.8 -  [code del]: "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
1.9 -
1.10 -definition
1.11    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
1.12          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
1.13    [code del]: "f -- a --> L =
1.14 @@ -31,23 +27,11 @@
1.15    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
1.16    [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
1.17
1.18 -subsection {* Neighborhood Filter *}
1.19 -
1.20 -lemma eventually_at:
1.21 -  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
1.22 -unfolding at_def
1.23 -apply (rule eventually_Abs_filter)
1.24 -apply (rule_tac x=1 in exI, simp)
1.25 -apply (clarify, rule_tac x=r in exI, simp)
1.26 -apply (clarify, rename_tac r s)
1.27 -apply (rule_tac x="min r s" in exI, simp)
1.28 -done
1.29 +subsection {* Limits of Functions *}
1.30
1.31  lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
1.32  unfolding LIM_def tendsto_def eventually_at ..
1.33
1.34 -subsection {* Limits of Functions *}
1.35 -
1.36  lemma metric_LIM_I:
1.37    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
1.38      \<Longrightarrow> f -- a --> L"
```