src/HOL/Lim.thy
changeset 29885 379e43e513c2
parent 29803 c56a5571f60a
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/Lim.thy	Fri Feb 13 08:00:46 2009 +1100
     1.2 +++ b/src/HOL/Lim.thy	Thu Feb 12 20:36:41 2009 -0800
     1.3 @@ -452,6 +452,11 @@
     1.4    shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
     1.5  by (rule LIM_inverse_fun [THEN LIM_compose])
     1.6  
     1.7 +lemma LIM_sgn:
     1.8 +  "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
     1.9 +unfolding sgn_div_norm
    1.10 +by (simp add: LIM_scaleR LIM_inverse LIM_norm)
    1.11 +
    1.12  
    1.13  subsection {* Continuity *}
    1.14  
    1.15 @@ -529,6 +534,10 @@
    1.16    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
    1.17    unfolding isCont_def by (rule LIM_power)
    1.18  
    1.19 +lemma isCont_sgn:
    1.20 +  "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
    1.21 +  unfolding isCont_def by (rule LIM_sgn)
    1.22 +
    1.23  lemma isCont_abs [simp]: "isCont abs (a::real)"
    1.24  by (rule isCont_rabs [OF isCont_ident])
    1.25