src/HOL/Limits.thy
changeset 44079 bcc60791b7b9
parent 41970 47d6e13d1710
child 44081 730f7cced3a6
     1.1 --- a/src/HOL/Limits.thy	Mon Aug 08 16:19:57 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Mon Aug 08 16:57:37 2011 -0700
     1.3 @@ -644,16 +644,6 @@
     1.4    "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
     1.5  unfolding tendsto_iff dist_norm by simp
     1.6  
     1.7 -lemma add_diff_add:
     1.8 -  fixes a b c d :: "'a::ab_group_add"
     1.9 -  shows "(a + c) - (b + d) = (a - b) + (c - d)"
    1.10 -by simp
    1.11 -
    1.12 -lemma minus_diff_minus:
    1.13 -  fixes a b :: "'a::ab_group_add"
    1.14 -  shows "(- a) - (- b) = - (a - b)"
    1.15 -by simp
    1.16 -
    1.17  lemma tendsto_add [tendsto_intros]:
    1.18    fixes a b :: "'a::real_normed_vector"
    1.19    shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
    1.20 @@ -748,11 +738,6 @@
    1.21    shows "Zfun (\<lambda>x. f x ** g x) net"
    1.22  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
    1.23  
    1.24 -lemma inverse_diff_inverse:
    1.25 -  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
    1.26 -   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
    1.27 -by (simp add: algebra_simps)
    1.28 -
    1.29  lemma Bfun_inverse_lemma:
    1.30    fixes x :: "'a::real_normed_div_algebra"
    1.31    shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"