equal
deleted
inserted
replaced
28 [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" |
28 [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" |
29 |
29 |
30 subsection {* Limits of Functions *} |
30 subsection {* Limits of Functions *} |
31 |
31 |
32 lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)" |
32 lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)" |
33 unfolding LIM_def tendsto_def eventually_at .. |
33 unfolding LIM_def tendsto_iff eventually_at .. |
34 |
34 |
35 lemma metric_LIM_I: |
35 lemma metric_LIM_I: |
36 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
36 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
37 \<Longrightarrow> f -- a --> L" |
37 \<Longrightarrow> f -- a --> L" |
38 by (simp add: LIM_def) |
38 by (simp add: LIM_def) |