src/HOL/Analysis/Linear_Algebra.thy
changeset 66420 bc0dab0e7b40
parent 66297 d425bdf419f5
child 66447 a1f5c5c26fa6
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Aug 13 23:45:45 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Aug 14 18:54:25 2017 +0100
     1.3 @@ -1482,6 +1482,22 @@
     1.4  lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
     1.5    by (rule norm_triangle_ineq [THEN le_less_trans])
     1.6  
     1.7 +lemma abs_triangle_half_r:
     1.8 +  fixes y :: "'a::linordered_field"
     1.9 +  shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
    1.10 +  by linarith
    1.11 +
    1.12 +lemma abs_triangle_half_l:
    1.13 +  fixes y :: "'a::linordered_field"
    1.14 +  assumes "abs (x - y) < e / 2"
    1.15 +    and "abs (x' - y) < e / 2"
    1.16 +  shows "abs (x - x') < e"
    1.17 +  using assms by linarith
    1.18 +
    1.19 +lemma eps_leI: 
    1.20 +  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
    1.21 +  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
    1.22 +
    1.23  lemma sum_clauses:
    1.24    shows "sum f {} = 0"
    1.25      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"