equal
deleted
inserted
replaced
175 fixes e :: real |
175 fixes e :: real |
176 shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)" |
176 shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)" |
177 using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2] |
177 using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2] |
178 by (force simp add: power2_eq_square) |
178 by (force simp add: power2_eq_square) |
179 |
179 |
180 lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> inner x x = (0::real)" |
|
181 by simp (* TODO: delete *) |
|
182 |
|
183 lemma norm_triangle_sub: |
180 lemma norm_triangle_sub: |
184 fixes x y :: "'a::real_normed_vector" |
181 fixes x y :: "'a::real_normed_vector" |
185 shows "norm x \<le> norm y + norm (x - y)" |
182 shows "norm x \<le> norm y + norm (x - y)" |
186 using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) |
183 using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) |
187 |
184 |