generalize more lemmas about limits
authorhuffman
Tue May 04 15:44:42 2010 -0700 (2010-05-04)
changeset 366655d37a96de20c
parent 36663 f75b13ed4898
child 36666 1ea81fc5227a
generalize more lemmas about limits
src/HOL/Lim.thy
     1.1 --- a/src/HOL/Lim.thy	Tue May 04 13:11:15 2010 -0700
     1.2 +++ b/src/HOL/Lim.thy	Tue May 04 15:44:42 2010 -0700
     1.3 @@ -381,7 +381,7 @@
     1.4  lemmas LIM_of_real = of_real.LIM
     1.5  
     1.6  lemma LIM_power:
     1.7 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
     1.8 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
     1.9    assumes f: "f -- a --> l"
    1.10    shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
    1.11  by (induct n, simp, simp add: LIM_mult f)
    1.12 @@ -399,7 +399,7 @@
    1.13  by (rule LIM_inverse [OF LIM_ident a])
    1.14  
    1.15  lemma LIM_sgn:
    1.16 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.17 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.18    shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
    1.19  unfolding sgn_div_norm
    1.20  by (simp add: LIM_scaleR LIM_inverse LIM_norm)
    1.21 @@ -408,12 +408,12 @@
    1.22  subsection {* Continuity *}
    1.23  
    1.24  lemma LIM_isCont_iff:
    1.25 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
    1.26 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    1.27    shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
    1.28  by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
    1.29  
    1.30  lemma isCont_iff:
    1.31 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
    1.32 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    1.33    shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
    1.34  by (simp add: isCont_def LIM_isCont_iff)
    1.35  
    1.36 @@ -424,7 +424,7 @@
    1.37    unfolding isCont_def by (rule LIM_const)
    1.38  
    1.39  lemma isCont_norm:
    1.40 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.41 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.42    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
    1.43    unfolding isCont_def by (rule LIM_norm)
    1.44  
    1.45 @@ -432,27 +432,27 @@
    1.46    unfolding isCont_def by (rule LIM_rabs)
    1.47  
    1.48  lemma isCont_add:
    1.49 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.50 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.51    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
    1.52    unfolding isCont_def by (rule LIM_add)
    1.53  
    1.54  lemma isCont_minus:
    1.55 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.56 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.57    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
    1.58    unfolding isCont_def by (rule LIM_minus)
    1.59  
    1.60  lemma isCont_diff:
    1.61 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.62 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.63    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
    1.64    unfolding isCont_def by (rule LIM_diff)
    1.65  
    1.66  lemma isCont_mult:
    1.67 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra"
    1.68 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
    1.69    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
    1.70    unfolding isCont_def by (rule LIM_mult)
    1.71  
    1.72  lemma isCont_inverse:
    1.73 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra"
    1.74 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    1.75    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
    1.76    unfolding isCont_def by (rule LIM_inverse)
    1.77  
    1.78 @@ -495,12 +495,12 @@
    1.79    unfolding isCont_def by (rule LIM_of_real)
    1.80  
    1.81  lemma isCont_power:
    1.82 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.83 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.84    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
    1.85    unfolding isCont_def by (rule LIM_power)
    1.86  
    1.87  lemma isCont_sgn:
    1.88 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.89 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.90    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
    1.91    unfolding isCont_def by (rule LIM_sgn)
    1.92  
    1.93 @@ -508,7 +508,7 @@
    1.94  by (rule isCont_rabs [OF isCont_ident])
    1.95  
    1.96  lemma isCont_setsum:
    1.97 -  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
    1.98 +  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
    1.99    fixes A :: "'a set" assumes "finite A"
   1.100    shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
   1.101    using `finite A`