130 |
130 |
131 lemma metric_LIM_imp_LIM: |
131 lemma metric_LIM_imp_LIM: |
132 assumes f: "f -- a --> l" |
132 assumes f: "f -- a --> l" |
133 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |
133 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |
134 shows "g -- a --> m" |
134 shows "g -- a --> m" |
135 apply (rule tendstoI, drule tendstoD [OF f]) |
135 by (rule metric_tendsto_imp_tendsto [OF f], |
136 apply (simp add: eventually_at_topological, safe) |
136 auto simp add: eventually_at_topological le) |
137 apply (rule_tac x="S" in exI, safe) |
|
138 apply (drule_tac x="x" in bspec, safe) |
|
139 apply (erule (1) order_le_less_trans [OF le]) |
|
140 done |
|
141 |
137 |
142 lemma LIM_imp_LIM: |
138 lemma LIM_imp_LIM: |
143 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
139 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
144 fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector" |
140 fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector" |
145 assumes f: "f -- a --> l" |
141 assumes f: "f -- a --> l" |
146 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
142 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" |
147 shows "g -- a --> m" |
143 shows "g -- a --> m" |
148 apply (rule metric_LIM_imp_LIM [OF f]) |
144 by (rule metric_LIM_imp_LIM [OF f], |
149 apply (simp add: dist_norm le) |
145 simp add: dist_norm le) |
150 done |
|
151 |
146 |
152 lemma LIM_norm: |
147 lemma LIM_norm: |
153 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
148 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
154 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l" |
149 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l" |
155 by (rule tendsto_norm) |
150 by (rule tendsto_norm) |