158 |
158 |
159 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0" |
159 lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0" |
160 by (fold real_norm_def, rule LIM_norm_zero_iff) |
160 by (fold real_norm_def, rule LIM_norm_zero_iff) |
161 |
161 |
162 lemma LIM_const_not_eq: |
162 lemma LIM_const_not_eq: |
163 fixes a :: "'a::real_normed_div_algebra" |
163 fixes a :: "'a::real_normed_algebra_1" |
164 shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)" |
164 shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L" |
165 apply (simp add: LIM_eq) |
165 apply (simp add: LIM_eq) |
166 apply (rule_tac x="norm (k - L)" in exI, simp, safe) |
166 apply (rule_tac x="norm (k - L)" in exI, simp, safe) |
167 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) |
167 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) |
168 done |
168 done |
169 |
169 |
170 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] |
170 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] |
171 |
171 |
172 lemma LIM_const_eq: |
172 lemma LIM_const_eq: |
173 fixes a :: "'a::real_normed_div_algebra" |
173 fixes a :: "'a::real_normed_algebra_1" |
174 shows "(%x. k) -- a --> L ==> k = L" |
174 shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L" |
175 apply (rule ccontr) |
175 apply (rule ccontr) |
176 apply (blast dest: LIM_const_not_eq) |
176 apply (blast dest: LIM_const_not_eq) |
177 done |
177 done |
178 |
178 |
179 lemma LIM_unique: |
179 lemma LIM_unique: |
180 fixes a :: "'a::real_normed_div_algebra" |
180 fixes a :: "'a::real_normed_algebra_1" |
181 shows "[| f -- a --> L; f -- a --> M |] ==> L = M" |
181 shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M" |
182 apply (drule LIM_diff, assumption) |
182 apply (drule (1) LIM_diff) |
183 apply (auto dest!: LIM_const_eq) |
183 apply (auto dest!: LIM_const_eq) |
184 done |
184 done |
185 |
185 |
186 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a" |
186 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a" |
187 by (auto simp add: LIM_def) |
187 by (auto simp add: LIM_def) |