14 text{*Standard Definitions*} |
14 text{*Standard Definitions*} |
15 |
15 |
16 definition |
16 definition |
17 LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
17 LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
18 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where |
18 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where |
19 [code func del]: "f -- a --> L = |
19 [code del]: "f -- a --> L = |
20 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s |
20 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s |
21 --> norm (f x - L) < r)" |
21 --> norm (f x - L) < r)" |
22 |
22 |
23 definition |
23 definition |
24 isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
24 isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
25 "isCont f a = (f -- a --> (f a))" |
25 "isCont f a = (f -- a --> (f a))" |
26 |
26 |
27 definition |
27 definition |
28 isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
28 isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
29 [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)" |
29 [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)" |
30 |
30 |
31 |
31 |
32 subsection {* Limits of Functions *} |
32 subsection {* Limits of Functions *} |
33 |
33 |
34 subsubsection {* Purely standard proofs *} |
34 subsubsection {* Purely standard proofs *} |