src/HOL/Lim.thy
 changeset 44570 b93d1b3ee300 parent 44568 e6f291cb5810 child 44571 bd91b77c4cd6
equal 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"`