src/HOL/Analysis/Linear_Algebra.thy
changeset 66503 7685861f337d
parent 66486 ffaaa83543b2
child 66641 ff2e0115fea4
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 24 12:45:46 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 24 17:15:53 2017 +0100
     1.3 @@ -1457,10 +1457,6 @@
     1.4    shows "abs (x - x') < e"
     1.5    using assms by linarith
     1.6  
     1.7 -lemma eps_leI: 
     1.8 -  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
     1.9 -  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
    1.10 -
    1.11  lemma sum_clauses:
    1.12    shows "sum f {} = 0"
    1.13      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"