equal
deleted
inserted
replaced
84 apply (drule NSLIM_minus) |
84 apply (drule NSLIM_minus) |
85 apply (auto dest!: NSCLIM_const_eq [symmetric]) |
85 apply (auto dest!: NSCLIM_const_eq [symmetric]) |
86 done |
86 done |
87 |
87 |
88 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))" |
88 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))" |
89 by transfer (rule refl) |
|
90 |
|
91 lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))" |
|
92 by transfer (rule refl) |
|
93 |
|
94 lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))" |
|
95 by transfer (rule refl) |
89 by transfer (rule refl) |
96 |
90 |
97 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)" |
91 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)" |
98 by transfer (rule refl) |
92 by transfer (rule refl) |
99 |
93 |
120 "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) & |
114 "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) & |
121 (%x. Im(f x)) -- a --NS> Im(L))" |
115 (%x. Im(f x)) -- a --NS> Im(L))" |
122 apply (auto intro: NSLIM_Re NSLIM_Im) |
116 apply (auto intro: NSLIM_Re NSLIM_Im) |
123 apply (auto simp add: NSLIM_def starfun_Re starfun_Im) |
117 apply (auto simp add: NSLIM_def starfun_Re starfun_Im) |
124 apply (auto dest!: spec) |
118 apply (auto dest!: spec) |
125 apply (simp add: starfunC_approx_Re_Im_iff starfun_Re starfun_Im) |
119 apply (simp add: hcomplex_approx_iff) |
126 done |
120 done |
127 |
121 |
128 lemma LIM_CRLIM_Re_Im_iff: |
122 lemma LIM_CRLIM_Re_Im_iff: |
129 "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) & |
123 "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) & |
130 (%x. Im(f x)) -- a --> Im(L))" |
124 (%x. Im(f x)) -- a --> Im(L))" |