83 |
83 |
84 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
84 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
85 |
85 |
86 lemma LIM_zero: |
86 lemma LIM_zero: |
87 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
87 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
88 shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0" |
88 shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F" |
89 unfolding tendsto_iff dist_norm by simp |
89 unfolding tendsto_iff dist_norm by simp |
90 |
90 |
91 lemma LIM_zero_cancel: |
91 lemma LIM_zero_cancel: |
92 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
92 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" |
93 shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l" |
93 shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F" |
94 unfolding tendsto_iff dist_norm by simp |
94 unfolding tendsto_iff dist_norm by simp |
95 |
95 |
96 lemma LIM_zero_iff: |
96 lemma LIM_zero_iff: |
97 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
97 fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
98 shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l" |
98 shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F" |
99 unfolding tendsto_iff dist_norm by simp |
99 unfolding tendsto_iff dist_norm by simp |
100 |
100 |
101 lemma metric_LIM_imp_LIM: |
101 lemma metric_LIM_imp_LIM: |
102 assumes f: "f -- a --> l" |
102 assumes f: "f -- a --> l" |
103 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |
103 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |