src/HOL/Analysis/Linear_Algebra.thy
 changeset 69513 42e08052dae8 parent 69510 0f31dd2e540d child 69516 09bb8f470959
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:34 2018 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:36 2018 +0100
1.3 @@ -76,12 +76,6 @@
1.4    using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
1.5    unfolding dist_norm[symmetric] .
1.6
1.7 -lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
1.8 -  by (rule norm_triangle_ineq [THEN order_trans])
1.9 -
1.10 -lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
1.11 -  by (rule norm_triangle_ineq [THEN le_less_trans])
1.12 -
1.13  lemma abs_triangle_half_r:
1.14    fixes y :: "'a::linordered_field"
1.15    shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
1.16 @@ -99,13 +93,6 @@
1.17      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
1.18    by (auto simp add: insert_absorb)
1.19
1.20 -lemma sum_norm_bound:
1.21 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.22 -  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
1.23 -  shows "norm (sum f S) \<le> of_nat (card S)*K"
1.24 -  using sum_norm_le[OF K] sum_constant[symmetric]
1.25 -  by simp
1.26 -
1.27  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
1.28  proof
1.29    assume "\<forall>x. x \<bullet> y = x \<bullet> z"
```