src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51361 21e5b6efb317
parent 51351 dd1dd470690b
child 51362 dac3f564a98d
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 06 16:56:21 2013 +0100
     1.3 @@ -4159,95 +4159,102 @@
     1.4  
     1.5  subsubsection {* Structural rules for pointwise continuity *}
     1.6  
     1.7 -lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
     1.8 +ML {*
     1.9 +
    1.10 +structure Continuous_Intros = Named_Thms
    1.11 +(
    1.12 +  val name = @{binding continuous_intros}
    1.13 +  val description = "Structural introduction rules for pointwise continuity"
    1.14 +)
    1.15 +
    1.16 +*}
    1.17 +
    1.18 +setup Continuous_Intros.setup
    1.19 +
    1.20 +lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)"
    1.21    unfolding continuous_within by (rule tendsto_ident_at_within)
    1.22  
    1.23 -lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)"
    1.24 +lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)"
    1.25    unfolding continuous_at by (rule tendsto_ident_at)
    1.26  
    1.27 -lemma continuous_const: "continuous F (\<lambda>x. c)"
    1.28 +lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)"
    1.29    unfolding continuous_def by (rule tendsto_const)
    1.30  
    1.31 -lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
    1.32 +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
    1.33    unfolding continuous_def by (rule tendsto_fst)
    1.34  
    1.35 -lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
    1.36 +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
    1.37    unfolding continuous_def by (rule tendsto_snd)
    1.38  
    1.39 -lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
    1.40 +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
    1.41    unfolding continuous_def by (rule tendsto_Pair)
    1.42  
    1.43 -lemma continuous_dist:
    1.44 +lemma continuous_dist[continuous_intros]:
    1.45    assumes "continuous F f" and "continuous F g"
    1.46    shows "continuous F (\<lambda>x. dist (f x) (g x))"
    1.47    using assms unfolding continuous_def by (rule tendsto_dist)
    1.48  
    1.49 -lemma continuous_infdist:
    1.50 +lemma continuous_infdist[continuous_intros]:
    1.51    assumes "continuous F f"
    1.52    shows "continuous F (\<lambda>x. infdist (f x) A)"
    1.53    using assms unfolding continuous_def by (rule tendsto_infdist)
    1.54  
    1.55 -lemma continuous_norm:
    1.56 +lemma continuous_norm[continuous_intros]:
    1.57    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
    1.58    unfolding continuous_def by (rule tendsto_norm)
    1.59  
    1.60 -lemma continuous_infnorm:
    1.61 +lemma continuous_infnorm[continuous_intros]:
    1.62    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
    1.63    unfolding continuous_def by (rule tendsto_infnorm)
    1.64  
    1.65 -lemma continuous_add:
    1.66 +lemma continuous_add[continuous_intros]:
    1.67    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.68    shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    1.69    unfolding continuous_def by (rule tendsto_add)
    1.70  
    1.71 -lemma continuous_minus:
    1.72 +lemma continuous_minus[continuous_intros]:
    1.73    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.74    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
    1.75    unfolding continuous_def by (rule tendsto_minus)
    1.76  
    1.77 -lemma continuous_diff:
    1.78 +lemma continuous_diff[continuous_intros]:
    1.79    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.80    shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
    1.81    unfolding continuous_def by (rule tendsto_diff)
    1.82  
    1.83 -lemma continuous_scaleR:
    1.84 +lemma continuous_scaleR[continuous_intros]:
    1.85    fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    1.86    shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
    1.87    unfolding continuous_def by (rule tendsto_scaleR)
    1.88  
    1.89 -lemma continuous_mult:
    1.90 +lemma continuous_mult[continuous_intros]:
    1.91    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
    1.92    shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
    1.93    unfolding continuous_def by (rule tendsto_mult)
    1.94  
    1.95 -lemma continuous_inner:
    1.96 +lemma continuous_inner[continuous_intros]:
    1.97    assumes "continuous F f" and "continuous F g"
    1.98    shows "continuous F (\<lambda>x. inner (f x) (g x))"
    1.99    using assms unfolding continuous_def by (rule tendsto_inner)
   1.100  
   1.101 -lemma continuous_inverse:
   1.102 +lemma continuous_inverse[continuous_intros]:
   1.103    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.104    assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
   1.105    shows "continuous F (\<lambda>x. inverse (f x))"
   1.106    using assms unfolding continuous_def by (rule tendsto_inverse)
   1.107  
   1.108 -lemma continuous_at_within_inverse:
   1.109 +lemma continuous_at_within_inverse[continuous_intros]:
   1.110    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.111    assumes "continuous (at a within s) f" and "f a \<noteq> 0"
   1.112    shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
   1.113    using assms unfolding continuous_within by (rule tendsto_inverse)
   1.114  
   1.115 -lemma continuous_at_inverse:
   1.116 +lemma continuous_at_inverse[continuous_intros]:
   1.117    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
   1.118    assumes "continuous (at a) f" and "f a \<noteq> 0"
   1.119    shows "continuous (at a) (\<lambda>x. inverse (f x))"
   1.120    using assms unfolding continuous_at by (rule tendsto_inverse)
   1.121  
   1.122 -lemmas continuous_intros = continuous_at_id continuous_within_id
   1.123 -  continuous_const continuous_dist continuous_norm continuous_infnorm
   1.124 -  continuous_add continuous_minus continuous_diff continuous_scaleR continuous_mult
   1.125 -  continuous_inner continuous_at_inverse continuous_at_within_inverse
   1.126 -
   1.127  subsubsection {* Structural rules for setwise continuity *}
   1.128  
   1.129  lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"