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"