src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44531 1d477a2b1572
parent 44530 adb18b07b341
child 44533 7abe4a59f75d
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 16:50:55 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 19:41:38 2011 -0700
     1.3 @@ -3473,16 +3473,10 @@
     1.4  
     1.5  text{* Same thing for setwise continuity. *}
     1.6  
     1.7 -lemma continuous_on_const:
     1.8 - "continuous_on s (\<lambda>x. c)"
     1.9 +lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
    1.10    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.11  
    1.12 -lemma continuous_on_cmul:
    1.13 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.14 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
    1.15 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.16 -
    1.17 -lemma continuous_on_neg:
    1.18 +lemma continuous_on_minus:
    1.19    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.20    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
    1.21    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.22 @@ -3493,12 +3487,46 @@
    1.23             \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
    1.24    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.25  
    1.26 -lemma continuous_on_sub:
    1.27 +lemma continuous_on_diff:
    1.28    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.29    shows "continuous_on s f \<Longrightarrow> continuous_on s g
    1.30             \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
    1.31    unfolding continuous_on_def by (auto intro: tendsto_intros)
    1.32  
    1.33 +lemma (in bounded_linear) continuous_on:
    1.34 +  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
    1.35 +  unfolding continuous_on_def by (fast intro: tendsto)
    1.36 +
    1.37 +lemma (in bounded_bilinear) continuous_on:
    1.38 +  "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
    1.39 +  unfolding continuous_on_def by (fast intro: tendsto)
    1.40 +
    1.41 +lemma continuous_on_scaleR:
    1.42 +  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.43 +  assumes "continuous_on s f" and "continuous_on s g"
    1.44 +  shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
    1.45 +  using bounded_bilinear_scaleR assms
    1.46 +  by (rule bounded_bilinear.continuous_on)
    1.47 +
    1.48 +lemma continuous_on_mult:
    1.49 +  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
    1.50 +  assumes "continuous_on s f" and "continuous_on s g"
    1.51 +  shows "continuous_on s (\<lambda>x. f x * g x)"
    1.52 +  using bounded_bilinear_mult assms
    1.53 +  by (rule bounded_bilinear.continuous_on)
    1.54 +
    1.55 +lemma continuous_on_inner:
    1.56 +  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
    1.57 +  assumes "continuous_on s f" and "continuous_on s g"
    1.58 +  shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
    1.59 +  using bounded_bilinear_inner assms
    1.60 +  by (rule bounded_bilinear.continuous_on)
    1.61 +
    1.62 +lemma continuous_on_euclidean_component:
    1.63 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
    1.64 +  using bounded_linear_euclidean_component
    1.65 +  by (rule bounded_linear.continuous_on)
    1.66 +
    1.67  text{* Same thing for uniform continuity, using sequential formulations. *}
    1.68  
    1.69  lemma uniformly_continuous_on_const:
    1.70 @@ -3942,28 +3970,10 @@
    1.71  lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
    1.72    continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
    1.73  
    1.74 -lemma continuous_on_vmul:
    1.75 -  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
    1.76 -  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
    1.77 -  unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
    1.78 -
    1.79 -lemma continuous_on_mul:
    1.80 -  fixes c :: "'a::metric_space \<Rightarrow> real"
    1.81 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.82 -  shows "continuous_on s c \<Longrightarrow> continuous_on s f
    1.83 -             ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
    1.84 -  unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
    1.85 -
    1.86 -lemma continuous_on_mul_real:
    1.87 -  fixes f :: "'a::metric_space \<Rightarrow> real"
    1.88 -  fixes g :: "'a::metric_space \<Rightarrow> real"
    1.89 -  shows "continuous_on s f \<Longrightarrow> continuous_on s g
    1.90 -             ==> continuous_on s (\<lambda>x. f x * g x)"
    1.91 -  using continuous_on_mul[of s f g] unfolding real_scaleR_def .
    1.92 -
    1.93  lemmas continuous_on_intros = continuous_on_add continuous_on_const
    1.94 -  continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
    1.95 -  continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
    1.96 +  continuous_on_id continuous_on_compose continuous_on_minus
    1.97 +  continuous_on_diff continuous_on_scaleR continuous_on_mult
    1.98 +  continuous_on_inner continuous_on_euclidean_component
    1.99    uniformly_continuous_on_add uniformly_continuous_on_const
   1.100    uniformly_continuous_on_id uniformly_continuous_on_compose
   1.101    uniformly_continuous_on_cmul uniformly_continuous_on_neg
   1.102 @@ -5110,11 +5120,6 @@
   1.103  lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
   1.104    unfolding euclidean_component_def by (rule continuous_at_inner)
   1.105  
   1.106 -lemma continuous_on_inner:
   1.107 -  fixes s :: "'a::real_inner set"
   1.108 -  shows "continuous_on s (inner a)"
   1.109 -  unfolding continuous_on by (rule ballI) (intro tendsto_intros)
   1.110 -
   1.111  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
   1.112    by (simp add: closed_Collect_le)
   1.113  
   1.114 @@ -5391,8 +5396,7 @@
   1.115    unfolding homeomorphic_minimal
   1.116    apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
   1.117    apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
   1.118 -  using assms apply auto
   1.119 -  using continuous_on_cmul[OF continuous_on_id] by auto
   1.120 +  using assms by (auto simp add: continuous_on_intros)
   1.121  
   1.122  lemma homeomorphic_translation:
   1.123    fixes s :: "'a::real_normed_vector set"