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
```