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.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"
```