14 text{*Nonstandard Definitions*} |
14 text{*Nonstandard Definitions*} |
15 |
15 |
16 definition |
16 definition |
17 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
17 NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
18 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where |
18 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where |
19 [code func del]: "f -- a --NS> L = |
19 [code del]: "f -- a --NS> L = |
20 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
20 (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
21 |
21 |
22 definition |
22 definition |
23 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
23 isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
24 --{*NS definition dispenses with limit notions*} |
24 --{*NS definition dispenses with limit notions*} |
25 [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a --> |
25 [code del]: "isNSCont f a = (\<forall>y. y @= star_of a --> |
26 ( *f* f) y @= star_of (f a))" |
26 ( *f* f) y @= star_of (f a))" |
27 |
27 |
28 definition |
28 definition |
29 isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
29 isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
30 [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
30 [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
31 |
31 |
32 |
32 |
33 subsection {* Limits of Functions *} |
33 subsection {* Limits of Functions *} |
34 |
34 |
35 lemma NSLIM_I: |
35 lemma NSLIM_I: |