equal
deleted
inserted
replaced
81 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
81 shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L" |
82 by (drule_tac k="- a" in LIM_offset, simp) |
82 by (drule_tac k="- a" in LIM_offset, simp) |
83 |
83 |
84 lemma LIM_const [simp]: "(%x. k) -- x --> k" |
84 lemma LIM_const [simp]: "(%x. k) -- x --> k" |
85 by (simp add: LIM_def) |
85 by (simp add: LIM_def) |
|
86 |
|
87 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp |
86 |
88 |
87 lemma LIM_add: |
89 lemma LIM_add: |
88 fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
90 fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector" |
89 assumes f: "f -- a --> L" and g: "g -- a --> M" |
91 assumes f: "f -- a --> L" and g: "g -- a --> M" |
90 shows "(\<lambda>x. f x + g x) -- a --> (L + M)" |
92 shows "(\<lambda>x. f x + g x) -- a --> (L + M)" |