modernize lemmas about 'continuous' and 'continuous_on';
authorhuffman
Thu Sep 01 09:02:14 2011 -0700 (2011-09-01)
changeset 44647e4de7750cdeb
parent 44646 a6047ddd9377
child 44648 897f32a827f2
modernize lemmas about 'continuous' and 'continuous_on';
improve automation of continuity proofs;
NEWS
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/NEWS	Thu Sep 01 07:31:33 2011 -0700
     1.2 +++ b/NEWS	Thu Sep 01 09:02:14 2011 -0700
     1.3 @@ -201,7 +201,8 @@
     1.4    Cauchy_vector    ~> vec_CauchyI
     1.5  
     1.6  * Session Multivariate_Analysis: Several duplicate theorems have been
     1.7 -removed, and other theorems have been renamed. INCOMPATIBILITY.
     1.8 +removed, and other theorems have been renamed or replaced with more
     1.9 +general versions. INCOMPATIBILITY.
    1.10  
    1.11    eventually_conjI ~> eventually_conj
    1.12    eventually_and ~> eventually_conj_iff
    1.13 @@ -222,6 +223,17 @@
    1.14    Lim_inner ~> tendsto_inner [OF tendsto_const]
    1.15    dot_lsum ~> inner_setsum_left
    1.16    dot_rsum ~> inner_setsum_right
    1.17 +  continuous_cmul ~> continuous_scaleR [OF continuous_const]
    1.18 +  continuous_neg ~> continuous_minus
    1.19 +  continuous_sub ~> continuous_diff
    1.20 +  continuous_vmul ~> continuous_scaleR [OF _ continuous_const]
    1.21 +  continuous_mul ~> continuous_scaleR
    1.22 +  continuous_inv ~> continuous_inverse
    1.23 +  continuous_at_within_inv ~> continuous_at_within_inverse
    1.24 +  continuous_at_inv ~> continuous_at_inverse
    1.25 +  continuous_at_norm ~> continuous_norm [OF continuous_at_id]
    1.26 +  continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]
    1.27 +  continuous_at_component ~> continuous_component [OF continuous_at_id]
    1.28    continuous_on_neg ~> continuous_on_minus
    1.29    continuous_on_sub ~> continuous_on_diff
    1.30    continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
    1.31 @@ -229,6 +241,8 @@
    1.32    continuous_on_mul ~> continuous_on_scaleR
    1.33    continuous_on_mul_real ~> continuous_on_mult
    1.34    continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
    1.35 +  continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]
    1.36 +  continuous_on_inverse ~> continuous_on_inv
    1.37    subset_interior ~> interior_mono
    1.38    subset_closure ~> closure_mono
    1.39    closure_univ ~> closure_UNIV
     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
     2.3 @@ -1075,11 +1075,13 @@
     2.4    unfolding nth_conv_component
     2.5    using component_le_infnorm[of x] .
     2.6  
     2.7 -lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
     2.8 -unfolding continuous_at by (intro tendsto_intros)
     2.9 +lemma continuous_component:
    2.10 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
    2.11 +  unfolding continuous_def by (rule tendsto_vec_nth)
    2.12  
    2.13 -lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
    2.14 -unfolding continuous_on_def by (intro ballI tendsto_intros)
    2.15 +lemma continuous_on_component:
    2.16 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
    2.17 +  unfolding continuous_on_def by (fast intro: tendsto_vec_nth)
    2.18  
    2.19  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
    2.20    by (simp add: Collect_all_eq closed_INT closed_Collect_le)
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
     3.3 @@ -3304,8 +3304,8 @@
     3.4      by auto
     3.5    have *:"\<And>x A B. x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A\<inter>B \<noteq> {}" by blast
     3.6    have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
     3.7 -    apply(rule, rule continuous_vmul)
     3.8 -    apply(rule continuous_at_id) by(rule compact_interval)
     3.9 +    apply(rule, intro continuous_intros)
    3.10 +    by(rule compact_interval)
    3.11    moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R x} \<inter> s \<noteq> {}" apply(rule *[OF _ assms(2)])
    3.12      unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos)
    3.13    ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
    3.14 @@ -3343,11 +3343,8 @@
    3.15  
    3.16    have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on)
    3.17      apply rule unfolding pi_def
    3.18 -    apply (rule continuous_mul)
    3.19 -    apply (rule continuous_at_inv[unfolded o_def])
    3.20 -    apply (rule continuous_at_norm)
    3.21 +    apply (intro continuous_intros)
    3.22      apply simp
    3.23 -    apply (rule continuous_at_id)
    3.24      done
    3.25    def sphere \<equiv> "{x::'a. norm x = 1}"
    3.26    have pi:"\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *\<^sub>R x) = pi x" unfolding pi_def sphere_def by auto
    3.27 @@ -3433,7 +3430,7 @@
    3.28      prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
    3.29      fix x::"'a" assume as:"x \<in> cball 0 1"
    3.30      thus "continuous (at x) (\<lambda>x. norm x *\<^sub>R surf (pi x))" proof(cases "x=0")
    3.31 -      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_norm)
    3.32 +      case False thus ?thesis apply (intro continuous_intros)
    3.33          using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
    3.34      next obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
    3.35        hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer 
     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 07:31:33 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 09:02:14 2011 -0700
     4.3 @@ -1049,7 +1049,7 @@
     4.4    show ?thesis
     4.5      apply(rule has_derivative_inverse_basic_x[OF assms(6-8)])
     4.6      apply(rule continuous_on_interior[OF _ assms(3)])
     4.7 -    apply(rule continuous_on_inverse[OF assms(4,1)])
     4.8 +    apply(rule continuous_on_inv[OF assms(4,1)])
     4.9      apply(rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
    4.10      by(rule, rule *, assumption)
    4.11  qed
     5.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 01 07:31:33 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 01 09:02:14 2011 -0700
     5.3 @@ -41,15 +41,19 @@
     5.4      hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
     5.5    have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
     5.6    have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
     5.7 -  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
     5.8 -    prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
     5.9 -    apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
    5.10 -    apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
    5.11 -    apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
    5.12 +  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
    5.13 +    apply(intro continuous_on_intros continuous_on_component)
    5.14 +    unfolding * apply(rule assms)+
    5.15 +    apply(subst sqprojection_def)
    5.16 +    apply(intro continuous_on_intros)
    5.17 +    apply(simp add: infnorm_eq_0 x0)
    5.18 +    apply(rule linear_continuous_on)
    5.19 +  proof-
    5.20      show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
    5.21        show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
    5.22          apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
    5.23 -        unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
    5.24 +        unfolding negatex_def by(auto simp add:vector_2 ) qed
    5.25 +  qed
    5.26    have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
    5.27      case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
    5.28      hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
     6.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 01 07:31:33 2011 -0700
     6.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 01 09:02:14 2011 -0700
     6.3 @@ -567,9 +567,8 @@
     6.4      unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
     6.5    have **:"{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_eqI,rule)
     6.6      unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
     6.7 -  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
     6.8 -    apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
     6.9 -    apply(rule continuous_at_norm[unfolded o_def]) by auto
    6.10 +  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
    6.11 +    unfolding field_divide_inverse by (simp add: continuous_on_intros)
    6.12    thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
    6.13      by(auto intro!: path_connected_continuous_image continuous_on_intros)
    6.14  qed
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
     7.3 @@ -3332,35 +3332,103 @@
     7.4  
     7.5  text{* Combination results for pointwise continuity. *}
     7.6  
     7.7 -lemma continuous_const: "continuous net (\<lambda>x. c)"
     7.8 -  by (auto simp add: continuous_def tendsto_const)
     7.9 -
    7.10 -lemma continuous_cmul:
    7.11 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.12 -  shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
    7.13 -  by (auto simp add: continuous_def intro: tendsto_intros)
    7.14 -
    7.15 -lemma continuous_neg:
    7.16 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.17 -  shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
    7.18 -  by (auto simp add: continuous_def tendsto_minus)
    7.19 +lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
    7.20 +  unfolding continuous_within by (rule tendsto_ident_at_within)
    7.21 +
    7.22 +lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)"
    7.23 +  unfolding continuous_at by (rule tendsto_ident_at)
    7.24 +
    7.25 +lemma continuous_const: "continuous F (\<lambda>x. c)"
    7.26 +  unfolding continuous_def by (rule tendsto_const)
    7.27 +
    7.28 +lemma continuous_dist:
    7.29 +  assumes "continuous F f" and "continuous F g"
    7.30 +  shows "continuous F (\<lambda>x. dist (f x) (g x))"
    7.31 +  using assms unfolding continuous_def by (rule tendsto_dist)
    7.32 +
    7.33 +lemma continuous_norm:
    7.34 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
    7.35 +  unfolding continuous_def by (rule tendsto_norm)
    7.36 +
    7.37 +lemma continuous_infnorm:
    7.38 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
    7.39 +  unfolding continuous_def by (rule tendsto_infnorm)
    7.40  
    7.41  lemma continuous_add:
    7.42    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.43 -  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
    7.44 -  by (auto simp add: continuous_def tendsto_add)
    7.45 -
    7.46 -lemma continuous_sub:
    7.47 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
    7.48 +  unfolding continuous_def by (rule tendsto_add)
    7.49 +
    7.50 +lemma continuous_minus:
    7.51 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.52 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
    7.53 +  unfolding continuous_def by (rule tendsto_minus)
    7.54 +
    7.55 +lemma continuous_diff:
    7.56    fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.57 -  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
    7.58 -  by (auto simp add: continuous_def tendsto_diff)
    7.59 -
    7.60 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
    7.61 +  unfolding continuous_def by (rule tendsto_diff)
    7.62 +
    7.63 +lemma continuous_scaleR:
    7.64 +  fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
    7.65 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
    7.66 +  unfolding continuous_def by (rule tendsto_scaleR)
    7.67 +
    7.68 +lemma continuous_mult:
    7.69 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
    7.70 +  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
    7.71 +  unfolding continuous_def by (rule tendsto_mult)
    7.72 +
    7.73 +lemma continuous_inner:
    7.74 +  assumes "continuous F f" and "continuous F g"
    7.75 +  shows "continuous F (\<lambda>x. inner (f x) (g x))"
    7.76 +  using assms unfolding continuous_def by (rule tendsto_inner)
    7.77 +
    7.78 +lemma continuous_euclidean_component:
    7.79 +  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $$ i)"
    7.80 +  unfolding continuous_def by (rule tendsto_euclidean_component)
    7.81 +
    7.82 +lemma continuous_inverse:
    7.83 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
    7.84 +  assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
    7.85 +  shows "continuous F (\<lambda>x. inverse (f x))"
    7.86 +  using assms unfolding continuous_def by (rule tendsto_inverse)
    7.87 +
    7.88 +lemma continuous_at_within_inverse:
    7.89 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
    7.90 +  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
    7.91 +  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
    7.92 +  using assms unfolding continuous_within by (rule tendsto_inverse)
    7.93 +
    7.94 +lemma continuous_at_inverse:
    7.95 +  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
    7.96 +  assumes "continuous (at a) f" and "f a \<noteq> 0"
    7.97 +  shows "continuous (at a) (\<lambda>x. inverse (f x))"
    7.98 +  using assms unfolding continuous_at by (rule tendsto_inverse)
    7.99 +
   7.100 +lemmas continuous_intros = continuous_at_id continuous_within_id
   7.101 +  continuous_const continuous_dist continuous_norm continuous_infnorm
   7.102 +  continuous_add continuous_minus continuous_diff
   7.103 +  continuous_scaleR continuous_mult
   7.104 +  continuous_inner continuous_euclidean_component
   7.105 +  continuous_at_inverse continuous_at_within_inverse
   7.106  
   7.107  text{* Same thing for setwise continuity. *}
   7.108  
   7.109 +lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
   7.110 +  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
   7.111 +
   7.112  lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
   7.113    unfolding continuous_on_def by (auto intro: tendsto_intros)
   7.114  
   7.115 +lemma continuous_on_norm:
   7.116 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
   7.117 +  unfolding continuous_on_def by (fast intro: tendsto_norm)
   7.118 +
   7.119 +lemma continuous_on_infnorm:
   7.120 +  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
   7.121 +  unfolding continuous_on by (fast intro: tendsto_infnorm)
   7.122 +
   7.123  lemma continuous_on_minus:
   7.124    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   7.125    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
   7.126 @@ -3412,8 +3480,18 @@
   7.127    using bounded_linear_euclidean_component
   7.128    by (rule bounded_linear.continuous_on)
   7.129  
   7.130 +lemma continuous_on_inverse:
   7.131 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   7.132 +  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   7.133 +  shows "continuous_on s (\<lambda>x. inverse (f x))"
   7.134 +  using assms unfolding continuous_on by (fast intro: tendsto_inverse)
   7.135 +
   7.136  text{* Same thing for uniform continuity, using sequential formulations. *}
   7.137  
   7.138 +lemma uniformly_continuous_on_id:
   7.139 + "uniformly_continuous_on s (\<lambda>x. x)"
   7.140 +  unfolding uniformly_continuous_on_def by auto
   7.141 +
   7.142  lemma uniformly_continuous_on_const:
   7.143   "uniformly_continuous_on s (\<lambda>x. c)"
   7.144    unfolding uniformly_continuous_on_def by simp
   7.145 @@ -3465,24 +3543,6 @@
   7.146    using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
   7.147    using uniformly_continuous_on_neg[of s g] by auto
   7.148  
   7.149 -text{* Identity function is continuous in every sense. *}
   7.150 -
   7.151 -lemma continuous_within_id:
   7.152 - "continuous (at a within s) (\<lambda>x. x)"
   7.153 -  unfolding continuous_within by (rule Lim_at_within [OF tendsto_ident_at])
   7.154 -
   7.155 -lemma continuous_at_id:
   7.156 - "continuous (at a) (\<lambda>x. x)"
   7.157 -  unfolding continuous_at by (rule tendsto_ident_at)
   7.158 -
   7.159 -lemma continuous_on_id:
   7.160 - "continuous_on s (\<lambda>x. x)"
   7.161 -  unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
   7.162 -
   7.163 -lemma uniformly_continuous_on_id:
   7.164 - "uniformly_continuous_on s (\<lambda>x. x)"
   7.165 -  unfolding uniformly_continuous_on_def by auto
   7.166 -
   7.167  text{* Continuity of all kinds is preserved under composition. *}
   7.168  
   7.169  lemma continuous_within_topological:
   7.170 @@ -3522,6 +3582,16 @@
   7.171    thus ?thesis using assms unfolding uniformly_continuous_on_def by auto
   7.172  qed
   7.173  
   7.174 +lemmas continuous_on_intros = continuous_on_id continuous_on_const
   7.175 +  continuous_on_compose continuous_on_norm continuous_on_infnorm
   7.176 +  continuous_on_add continuous_on_minus continuous_on_diff
   7.177 +  continuous_on_scaleR continuous_on_mult continuous_on_inverse
   7.178 +  continuous_on_inner continuous_on_euclidean_component
   7.179 +  uniformly_continuous_on_add uniformly_continuous_on_const
   7.180 +  uniformly_continuous_on_id uniformly_continuous_on_compose
   7.181 +  uniformly_continuous_on_cmul uniformly_continuous_on_neg
   7.182 +  uniformly_continuous_on_sub
   7.183 +
   7.184  text{* Continuity in terms of open preimages. *}
   7.185  
   7.186  lemma continuous_at_open:
   7.187 @@ -3804,8 +3874,9 @@
   7.188    fixes s :: "'a::real_normed_vector set"
   7.189    assumes "open s"  shows "open((\<lambda>x. a + x) ` s)"
   7.190  proof-
   7.191 -  { fix x have "continuous (at x) (\<lambda>x. x - a)" using continuous_sub[of "at x" "\<lambda>x. x" "\<lambda>x. a"] continuous_at_id[of x] continuous_const[of "at x" a] by auto  }
   7.192 -  moreover have "{x. x - a \<in> s}  = op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
   7.193 +  { fix x have "continuous (at x) (\<lambda>x. x - a)"
   7.194 +      by (intro continuous_diff continuous_at_id continuous_const) }
   7.195 +  moreover have "{x. x - a \<in> s} = op + a ` s" by force
   7.196    ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s] using assms by auto
   7.197  qed
   7.198  
   7.199 @@ -3838,53 +3909,6 @@
   7.200    thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
   7.201  qed
   7.202  
   7.203 -text {* We can now extend limit compositions to consider the scalar multiplier. *}
   7.204 -
   7.205 -lemma continuous_vmul:
   7.206 -  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
   7.207 -  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
   7.208 -  unfolding continuous_def by (intro tendsto_intros)
   7.209 -
   7.210 -lemma continuous_mul:
   7.211 -  fixes c :: "'a::metric_space \<Rightarrow> real"
   7.212 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   7.213 -  shows "continuous net c \<Longrightarrow> continuous net f
   7.214 -             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
   7.215 -  unfolding continuous_def by (intro tendsto_intros)
   7.216 -
   7.217 -lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
   7.218 -  continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
   7.219 -
   7.220 -lemmas continuous_on_intros = continuous_on_add continuous_on_const
   7.221 -  continuous_on_id continuous_on_compose continuous_on_minus
   7.222 -  continuous_on_diff continuous_on_scaleR continuous_on_mult
   7.223 -  continuous_on_inner continuous_on_euclidean_component
   7.224 -  uniformly_continuous_on_add uniformly_continuous_on_const
   7.225 -  uniformly_continuous_on_id uniformly_continuous_on_compose
   7.226 -  uniformly_continuous_on_cmul uniformly_continuous_on_neg
   7.227 -  uniformly_continuous_on_sub
   7.228 -
   7.229 -text {* And so we have continuity of inverse. *}
   7.230 -
   7.231 -lemma continuous_inv:
   7.232 -  fixes f :: "'a::metric_space \<Rightarrow> real"
   7.233 -  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
   7.234 -           ==> continuous net (inverse o f)"
   7.235 -  unfolding continuous_def using Lim_inv by auto
   7.236 -
   7.237 -lemma continuous_at_within_inv:
   7.238 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
   7.239 -  assumes "continuous (at a within s) f" "f a \<noteq> 0"
   7.240 -  shows "continuous (at a within s) (inverse o f)"
   7.241 -  using assms unfolding continuous_within o_def
   7.242 -  by (intro tendsto_intros)
   7.243 -
   7.244 -lemma continuous_at_inv:
   7.245 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
   7.246 -  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
   7.247 -         ==> continuous (at a) (inverse o f) "
   7.248 -  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
   7.249 -
   7.250  text {* Topological properties of linear functions. *}
   7.251  
   7.252  lemma linear_lim_0:
   7.253 @@ -3999,7 +4023,7 @@
   7.254  
   7.255  text{* Continuity of inverse function on compact domain. *}
   7.256  
   7.257 -lemma continuous_on_inverse:
   7.258 +lemma continuous_on_inv:
   7.259    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   7.260      (* TODO: can this be generalized more? *)
   7.261    assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
   7.262 @@ -4090,17 +4114,6 @@
   7.263    shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
   7.264    unfolding continuous_on_iff dist_norm by simp
   7.265  
   7.266 -lemma continuous_at_norm: "continuous (at x) norm"
   7.267 -  unfolding continuous_at by (intro tendsto_intros)
   7.268 -
   7.269 -lemma continuous_on_norm: "continuous_on s norm"
   7.270 -unfolding continuous_on by (intro ballI tendsto_intros)
   7.271 -
   7.272 -lemma continuous_at_infnorm: "continuous (at x) infnorm"
   7.273 -  unfolding continuous_at Lim_at o_def unfolding dist_norm
   7.274 -  apply auto apply (rule_tac x=e in exI) apply auto
   7.275 -  using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
   7.276 -
   7.277  text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
   7.278  
   7.279  lemma compact_attains_sup:
   7.280 @@ -5219,7 +5232,7 @@
   7.281  
   7.282  lemma homeomorphism_compact:
   7.283    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   7.284 -    (* class constraint due to continuous_on_inverse *)
   7.285 +    (* class constraint due to continuous_on_inv *)
   7.286    assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
   7.287    shows "\<exists>g. homeomorphism s t f g"
   7.288  proof-
   7.289 @@ -5242,12 +5255,12 @@
   7.290    hence "g ` t = s" by auto
   7.291    ultimately
   7.292    show ?thesis unfolding homeomorphism_def homeomorphic_def
   7.293 -    apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inverse[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto
   7.294 +    apply(rule_tac x=g in exI) using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2) by auto
   7.295  qed
   7.296  
   7.297  lemma homeomorphic_compact:
   7.298    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
   7.299 -    (* class constraint due to continuous_on_inverse *)
   7.300 +    (* class constraint due to continuous_on_inv *)
   7.301    shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
   7.302            \<Longrightarrow> s homeomorphic t"
   7.303    unfolding homeomorphic_def by (metis homeomorphism_compact)