# HG changeset patch # User hoelzl # Date 1362585381 -3600 # Node ID dac3f564a98d31a8c500509791ce4fad4ef7b5c2 # Parent 21e5b6efb317a1937cf8a400084319fc7087f984 changed continuous_on_intros into a named theorems collection diff -r 21e5b6efb317 -r dac3f564a98d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 @@ -4257,67 +4257,79 @@ subsubsection {* Structural rules for setwise continuity *} -lemma continuous_on_id: "continuous_on s (\x. x)" +ML {* + +structure Continuous_On_Intros = Named_Thms +( + val name = @{binding continuous_on_intros} + val description = "Structural introduction rules for setwise continuity" +) + +*} + +setup Continuous_On_Intros.setup + +lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\x. x)" unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) -lemma continuous_on_const: "continuous_on s (\x. c)" +lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\x. c)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma continuous_on_norm: +lemma continuous_on_norm[continuous_on_intros]: shows "continuous_on s f \ continuous_on s (\x. norm (f x))" unfolding continuous_on_def by (fast intro: tendsto_norm) -lemma continuous_on_infnorm: +lemma continuous_on_infnorm[continuous_on_intros]: shows "continuous_on s f \ continuous_on s (\x. infnorm (f x))" unfolding continuous_on by (fast intro: tendsto_infnorm) -lemma continuous_on_minus: +lemma continuous_on_minus[continuous_on_intros]: fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s (\x. - f x)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma continuous_on_add: +lemma continuous_on_add[continuous_on_intros]: fixes f g :: "'a::topological_space \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma continuous_on_diff: +lemma continuous_on_diff[continuous_on_intros]: fixes f g :: "'a::topological_space \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" unfolding continuous_on_def by (auto intro: tendsto_intros) -lemma (in bounded_linear) continuous_on: +lemma (in bounded_linear) continuous_on[continuous_on_intros]: "continuous_on s g \ continuous_on s (\x. f (g x))" unfolding continuous_on_def by (fast intro: tendsto) -lemma (in bounded_bilinear) continuous_on: +lemma (in bounded_bilinear) continuous_on[continuous_on_intros]: "\continuous_on s f; continuous_on s g\ \ continuous_on s (\x. f x ** g x)" unfolding continuous_on_def by (fast intro: tendsto) -lemma continuous_on_scaleR: +lemma continuous_on_scaleR[continuous_on_intros]: fixes g :: "'a::topological_space \ 'b::real_normed_vector" assumes "continuous_on s f" and "continuous_on s g" shows "continuous_on s (\x. f x *\<^sub>R g x)" using bounded_bilinear_scaleR assms by (rule bounded_bilinear.continuous_on) -lemma continuous_on_mult: +lemma continuous_on_mult[continuous_on_intros]: fixes g :: "'a::topological_space \ 'b::real_normed_algebra" assumes "continuous_on s f" and "continuous_on s g" shows "continuous_on s (\x. f x * g x)" using bounded_bilinear_mult assms by (rule bounded_bilinear.continuous_on) -lemma continuous_on_inner: +lemma continuous_on_inner[continuous_on_intros]: fixes g :: "'a::topological_space \ 'b::real_inner" assumes "continuous_on s f" and "continuous_on s g" shows "continuous_on s (\x. inner (f x) (g x))" using bounded_bilinear_inner assms by (rule bounded_bilinear.continuous_on) -lemma continuous_on_inverse: +lemma continuous_on_inverse[continuous_on_intros]: fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" assumes "continuous_on s f" and "\x\s. f x \ 0" shows "continuous_on s (\x. inverse (f x))" @@ -4325,15 +4337,15 @@ subsubsection {* Structural rules for uniform continuity *} -lemma uniformly_continuous_on_id: +lemma uniformly_continuous_on_id[continuous_on_intros]: shows "uniformly_continuous_on s (\x. x)" unfolding uniformly_continuous_on_def by auto -lemma uniformly_continuous_on_const: +lemma uniformly_continuous_on_const[continuous_on_intros]: shows "uniformly_continuous_on s (\x. c)" unfolding uniformly_continuous_on_def by simp -lemma uniformly_continuous_on_dist: +lemma uniformly_continuous_on_dist[continuous_on_intros]: fixes f g :: "'a::metric_space \ 'b::metric_space" assumes "uniformly_continuous_on s f" assumes "uniformly_continuous_on s g" @@ -4355,20 +4367,20 @@ unfolding dist_real_def by simp qed -lemma uniformly_continuous_on_norm: +lemma uniformly_continuous_on_norm[continuous_on_intros]: assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. norm (f x))" unfolding norm_conv_dist using assms by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) -lemma (in bounded_linear) uniformly_continuous_on: +lemma (in bounded_linear) uniformly_continuous_on[continuous_on_intros]: assumes "uniformly_continuous_on s g" shows "uniformly_continuous_on s (\x. f (g x))" using assms unfolding uniformly_continuous_on_sequentially unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] by (auto intro: tendsto_zero) -lemma uniformly_continuous_on_cmul: +lemma uniformly_continuous_on_cmul[continuous_on_intros]: fixes f :: "'a::metric_space \ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" @@ -4380,12 +4392,12 @@ shows "dist (- x) (- y) = dist x y" unfolding dist_norm minus_diff_minus norm_minus_cancel .. -lemma uniformly_continuous_on_minus: +lemma uniformly_continuous_on_minus[continuous_on_intros]: fixes f :: "'a::metric_space \ 'b::real_normed_vector" shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. - f x)" unfolding uniformly_continuous_on_def dist_minus . -lemma uniformly_continuous_on_add: +lemma uniformly_continuous_on_add[continuous_on_intros]: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" assumes "uniformly_continuous_on s g" @@ -4394,7 +4406,7 @@ unfolding dist_norm tendsto_norm_zero_iff add_diff_add by (auto intro: tendsto_add_zero) -lemma uniformly_continuous_on_diff: +lemma uniformly_continuous_on_diff[continuous_on_intros]: fixes f :: "'a::metric_space \ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g" shows "uniformly_continuous_on s (\x. f x - g x)" @@ -4411,13 +4423,13 @@ unfolding tendsto_def Limits.eventually_within eventually_at_topological by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto -lemma continuous_within_compose: +lemma continuous_within_compose[continuous_intros]: assumes "continuous (at x within s) f" assumes "continuous (at (f x) within f ` s) g" shows "continuous (at x within s) (g o f)" using assms unfolding continuous_within_topological by simp metis -lemma continuous_at_compose: +lemma continuous_at_compose[continuous_intros]: assumes "continuous (at x) f" and "continuous (at (f x)) g" shows "continuous (at x) (g o f)" proof- @@ -4427,11 +4439,11 @@ using continuous_within_compose[of x UNIV f g] by simp qed -lemma continuous_on_compose: +lemma continuous_on_compose[continuous_on_intros]: "continuous_on s f \ continuous_on (f ` s) g \ continuous_on s (g o f)" unfolding continuous_on_topological by simp metis -lemma uniformly_continuous_on_compose: +lemma uniformly_continuous_on_compose[continuous_on_intros]: assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g" shows "uniformly_continuous_on s (g o f)" proof- @@ -4442,17 +4454,6 @@ thus ?thesis using assms unfolding uniformly_continuous_on_def by auto qed -lemmas continuous_on_intros = continuous_on_id continuous_on_const - continuous_on_compose continuous_on_norm continuous_on_infnorm - continuous_on_add continuous_on_minus continuous_on_diff - continuous_on_scaleR continuous_on_mult continuous_on_inverse - continuous_on_inner - uniformly_continuous_on_id uniformly_continuous_on_const - uniformly_continuous_on_dist uniformly_continuous_on_norm - uniformly_continuous_on_compose uniformly_continuous_on_add - uniformly_continuous_on_minus uniformly_continuous_on_diff - uniformly_continuous_on_cmul - text{* Continuity in terms of open preimages. *} lemma continuous_at_open: