src/HOL/Lim.thy
 changeset 36665 5d37a96de20c parent 36662 621122eeb138 child 37767 a2b7a20d6ea3
```     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.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`
```