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_triangle_sub: |
|
181 fixes x y :: "'a::real_normed_vector" |
|
182 shows "norm x \<le> norm y + norm (x - y)" |
|
183 using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps) |
|
184 |
|
185 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y" |
180 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y" |
186 by (simp add: norm_eq_sqrt_inner) |
181 by (simp add: norm_eq_sqrt_inner) |
187 |
182 |
188 lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y" |
183 lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y" |
189 by (simp add: norm_eq_sqrt_inner) |
184 by (simp add: norm_eq_sqrt_inner) |