summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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)"