summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Wed, 06 Mar 2013 16:56:21 +0100 | |

changeset 51361 | 21e5b6efb317 |

parent 51360 | c4367ed99b5e |

child 51362 | dac3f564a98d |

changed continuous_intros into a named theorems collection

src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 06 16:56:21 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 06 16:56:21 2013 +0100 @@ -4159,95 +4159,102 @@ subsubsection {* Structural rules for pointwise continuity *} -lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)" +ML {* + +structure Continuous_Intros = Named_Thms +( + val name = @{binding continuous_intros} + val description = "Structural introduction rules for pointwise continuity" +) + +*} + +setup Continuous_Intros.setup + +lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)" unfolding continuous_within by (rule tendsto_ident_at_within) -lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)" +lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)" unfolding continuous_at by (rule tendsto_ident_at) -lemma continuous_const: "continuous F (\<lambda>x. c)" +lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)" unfolding continuous_def by (rule tendsto_const) -lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" +lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" unfolding continuous_def by (rule tendsto_fst) -lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" +lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" unfolding continuous_def by (rule tendsto_snd) -lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" +lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" unfolding continuous_def by (rule tendsto_Pair) -lemma continuous_dist: +lemma continuous_dist[continuous_intros]: assumes "continuous F f" and "continuous F g" shows "continuous F (\<lambda>x. dist (f x) (g x))" using assms unfolding continuous_def by (rule tendsto_dist) -lemma continuous_infdist: +lemma continuous_infdist[continuous_intros]: assumes "continuous F f" shows "continuous F (\<lambda>x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) -lemma continuous_norm: +lemma continuous_norm[continuous_intros]: shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" unfolding continuous_def by (rule tendsto_norm) -lemma continuous_infnorm: +lemma continuous_infnorm[continuous_intros]: shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" unfolding continuous_def by (rule tendsto_infnorm) -lemma continuous_add: +lemma continuous_add[continuous_intros]: fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" unfolding continuous_def by (rule tendsto_add) -lemma continuous_minus: +lemma continuous_minus[continuous_intros]: fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)" unfolding continuous_def by (rule tendsto_minus) -lemma continuous_diff: +lemma continuous_diff[continuous_intros]: fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" unfolding continuous_def by (rule tendsto_diff) -lemma continuous_scaleR: +lemma continuous_scaleR[continuous_intros]: fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)" unfolding continuous_def by (rule tendsto_scaleR) -lemma continuous_mult: +lemma continuous_mult[continuous_intros]: fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra" shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)" unfolding continuous_def by (rule tendsto_mult) -lemma continuous_inner: +lemma continuous_inner[continuous_intros]: assumes "continuous F f" and "continuous F g" shows "continuous F (\<lambda>x. inner (f x) (g x))" using assms unfolding continuous_def by (rule tendsto_inner) -lemma continuous_inverse: +lemma continuous_inverse[continuous_intros]: fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" assumes "continuous F f" and "f (netlimit F) \<noteq> 0" shows "continuous F (\<lambda>x. inverse (f x))" using assms unfolding continuous_def by (rule tendsto_inverse) -lemma continuous_at_within_inverse: +lemma continuous_at_within_inverse[continuous_intros]: fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" assumes "continuous (at a within s) f" and "f a \<noteq> 0" shows "continuous (at a within s) (\<lambda>x. inverse (f x))" using assms unfolding continuous_within by (rule tendsto_inverse) -lemma continuous_at_inverse: +lemma continuous_at_inverse[continuous_intros]: fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" assumes "continuous (at a) f" and "f a \<noteq> 0" shows "continuous (at a) (\<lambda>x. inverse (f x))" using assms unfolding continuous_at by (rule tendsto_inverse) -lemmas continuous_intros = continuous_at_id continuous_within_id - continuous_const continuous_dist continuous_norm continuous_infnorm - continuous_add continuous_minus continuous_diff continuous_scaleR continuous_mult - continuous_inner continuous_at_inverse continuous_at_within_inverse - subsubsection {* Structural rules for setwise continuity *} lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"