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"