src/HOL/Lim.thy
changeset 44570 b93d1b3ee300
parent 44568 e6f291cb5810
child 44571 bd91b77c4cd6
equal deleted inserted replaced
44569:44525dd281d4 44570:b93d1b3ee300
    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"