# HG changeset patch
# User huffman
# Date 1314892934 25200
# Node ID e4de7750cdebc1a7e256dfa734d05ff6af5a7ef2
# Parent  a6047ddd93778037580f43c8ec962ab2680364f9
modernize lemmas about 'continuous' and 'continuous_on';
improve automation of continuity proofs;

diff -r a6047ddd9377 -r e4de7750cdeb NEWS
--- a/NEWS	Thu Sep 01 07:31:33 2011 -0700
+++ b/NEWS	Thu Sep 01 09:02:14 2011 -0700
@@ -201,7 +201,8 @@
   Cauchy_vector    ~> vec_CauchyI
 
 * Session Multivariate_Analysis: Several duplicate theorems have been
-removed, and other theorems have been renamed. INCOMPATIBILITY.
+removed, and other theorems have been renamed or replaced with more
+general versions. INCOMPATIBILITY.
 
   eventually_conjI ~> eventually_conj
   eventually_and ~> eventually_conj_iff
@@ -222,6 +223,17 @@
   Lim_inner ~> tendsto_inner [OF tendsto_const]
   dot_lsum ~> inner_setsum_left
   dot_rsum ~> inner_setsum_right
+  continuous_cmul ~> continuous_scaleR [OF continuous_const]
+  continuous_neg ~> continuous_minus
+  continuous_sub ~> continuous_diff
+  continuous_vmul ~> continuous_scaleR [OF _ continuous_const]
+  continuous_mul ~> continuous_scaleR
+  continuous_inv ~> continuous_inverse
+  continuous_at_within_inv ~> continuous_at_within_inverse
+  continuous_at_inv ~> continuous_at_inverse
+  continuous_at_norm ~> continuous_norm [OF continuous_at_id]
+  continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]
+  continuous_at_component ~> continuous_component [OF continuous_at_id]
   continuous_on_neg ~> continuous_on_minus
   continuous_on_sub ~> continuous_on_diff
   continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
@@ -229,6 +241,8 @@
   continuous_on_mul ~> continuous_on_scaleR
   continuous_on_mul_real ~> continuous_on_mult
   continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
+  continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]
+  continuous_on_inverse ~> continuous_on_inv
   subset_interior ~> interior_mono
   subset_closure ~> closure_mono
   closure_univ ~> closure_UNIV
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -1075,11 +1075,13 @@
   unfolding nth_conv_component
   using component_le_infnorm[of x] .
 
-lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
-unfolding continuous_at by (intro tendsto_intros)
+lemma continuous_component:
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
+  unfolding continuous_def by (rule tendsto_vec_nth)
 
-lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on_def by (intro ballI tendsto_intros)
+lemma continuous_on_component:
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
+  unfolding continuous_on_def by (fast intro: tendsto_vec_nth)
 
 lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
   by (simp add: Collect_all_eq closed_INT closed_Collect_le)
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -3304,8 +3304,8 @@
     by auto
   have *:"\<And>x A B. x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A\<inter>B \<noteq> {}" by blast
   have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
-    apply(rule, rule continuous_vmul)
-    apply(rule continuous_at_id) by(rule compact_interval)
+    apply(rule, intro continuous_intros)
+    by(rule compact_interval)
   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)])
     unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos)
   ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
@@ -3343,11 +3343,8 @@
 
   have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on)
     apply rule unfolding pi_def
-    apply (rule continuous_mul)
-    apply (rule continuous_at_inv[unfolded o_def])
-    apply (rule continuous_at_norm)
+    apply (intro continuous_intros)
     apply simp
-    apply (rule continuous_at_id)
     done
   def sphere \<equiv> "{x::'a. norm x = 1}"
   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
@@ -3433,7 +3430,7 @@
     prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
     fix x::"'a" assume as:"x \<in> cball 0 1"
     thus "continuous (at x) (\<lambda>x. norm x *\<^sub>R surf (pi x))" proof(cases "x=0")
-      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_norm)
+      case False thus ?thesis apply (intro continuous_intros)
         using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
     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
       hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis 0" in ballE) defer 
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -1049,7 +1049,7 @@
   show ?thesis
     apply(rule has_derivative_inverse_basic_x[OF assms(6-8)])
     apply(rule continuous_on_interior[OF _ assms(3)])
-    apply(rule continuous_on_inverse[OF assms(4,1)])
+    apply(rule continuous_on_inv[OF assms(4,1)])
     apply(rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
     by(rule, rule *, assumption)
 qed
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -41,15 +41,19 @@
     hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
   have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
   have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
-  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
-    prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
-    apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
-    apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
-    apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
+  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
+    apply(intro continuous_on_intros continuous_on_component)
+    unfolding * apply(rule assms)+
+    apply(subst sqprojection_def)
+    apply(intro continuous_on_intros)
+    apply(simp add: infnorm_eq_0 x0)
+    apply(rule linear_continuous_on)
+  proof-
     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
       show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
         apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
-        unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
+        unfolding negatex_def by(auto simp add:vector_2 ) qed
+  qed
   have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
     case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
     hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -567,9 +567,8 @@
     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)
   have **:"{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_eqI,rule)
     unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
-  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
-    apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
-    apply(rule continuous_at_norm[unfolded o_def]) by auto
+  have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
+    unfolding field_divide_inverse by (simp add: continuous_on_intros)
   thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
     by(auto intro!: path_connected_continuous_image continuous_on_intros)
 qed
diff -r a6047ddd9377 -r e4de7750cdeb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 07:31:33 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
@@ -3332,35 +3332,103 @@
 
 text{* Combination results for pointwise continuity. *}
 
-lemma continuous_const: "continuous net (\<lambda>x. c)"
-  by (auto simp add: continuous_def tendsto_const)
-
-lemma continuous_cmul:
-  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
-  by (auto simp add: continuous_def intro: tendsto_intros)
-
-lemma continuous_neg:
-  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
-  by (auto simp add: continuous_def tendsto_minus)
+lemma continuous_within_id: "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)"
+  unfolding continuous_at by (rule tendsto_ident_at)
+
+lemma continuous_const: "continuous F (\<lambda>x. c)"
+  unfolding continuous_def by (rule tendsto_const)
+
+lemma continuous_dist:
+  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_norm:
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
+  unfolding continuous_def by (rule tendsto_norm)
+
+lemma continuous_infnorm:
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
+  unfolding continuous_def by (rule tendsto_infnorm)
 
 lemma continuous_add:
   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
-  by (auto simp add: continuous_def tendsto_add)
-
-lemma continuous_sub:
+  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:
+  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:
   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
-  by (auto simp add: continuous_def tendsto_diff)
-
+  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:
+  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:
+  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:
+  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_euclidean_component:
+  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $$ i)"
+  unfolding continuous_def by (rule tendsto_euclidean_component)
+
+lemma continuous_inverse:
+  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:
+  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:
+  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_euclidean_component
+  continuous_at_inverse continuous_at_within_inverse
 
 text{* Same thing for setwise continuity. *}
 
+lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
+  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
+
 lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
   unfolding continuous_on_def by (auto intro: tendsto_intros)
 
+lemma continuous_on_norm:
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
+  unfolding continuous_on_def by (fast intro: tendsto_norm)
+
+lemma continuous_on_infnorm:
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
+  unfolding continuous_on by (fast intro: tendsto_infnorm)
+
 lemma continuous_on_minus:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
@@ -3412,8 +3480,18 @@
   using bounded_linear_euclidean_component
   by (rule bounded_linear.continuous_on)
 
+lemma continuous_on_inverse:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+  shows "continuous_on s (\<lambda>x. inverse (f x))"
+  using assms unfolding continuous_on by (fast intro: tendsto_inverse)
+
 text{* Same thing for uniform continuity, using sequential formulations. *}
 
+lemma uniformly_continuous_on_id:
+ "uniformly_continuous_on s (\<lambda>x. x)"
+  unfolding uniformly_continuous_on_def by auto
+
 lemma uniformly_continuous_on_const:
  "uniformly_continuous_on s (\<lambda>x. c)"
   unfolding uniformly_continuous_on_def by simp
@@ -3465,24 +3543,6 @@
   using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
   using uniformly_continuous_on_neg[of s g] by auto
 
-text{* Identity function is continuous in every sense. *}
-
-lemma continuous_within_id:
- "continuous (at a within s) (\<lambda>x. x)"
-  unfolding continuous_within by (rule Lim_at_within [OF tendsto_ident_at])
-
-lemma continuous_at_id:
- "continuous (at a) (\<lambda>x. x)"
-  unfolding continuous_at by (rule tendsto_ident_at)
-
-lemma continuous_on_id:
- "continuous_on s (\<lambda>x. x)"
-  unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
-
-lemma uniformly_continuous_on_id:
- "uniformly_continuous_on s (\<lambda>x. x)"
-  unfolding uniformly_continuous_on_def by auto
-
 text{* Continuity of all kinds is preserved under composition. *}
 
 lemma continuous_within_topological:
@@ -3522,6 +3582,16 @@
   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 continuous_on_euclidean_component
+  uniformly_continuous_on_add uniformly_continuous_on_const
+  uniformly_continuous_on_id uniformly_continuous_on_compose
+  uniformly_continuous_on_cmul uniformly_continuous_on_neg
+  uniformly_continuous_on_sub
+
 text{* Continuity in terms of open preimages. *}
 
 lemma continuous_at_open:
@@ -3804,8 +3874,9 @@
   fixes s :: "'a::real_normed_vector set"
   assumes "open s"  shows "open((\<lambda>x. a + x) ` s)"
 proof-
-  { 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  }
-  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
+  { fix x have "continuous (at x) (\<lambda>x. x - a)"
+      by (intro continuous_diff continuous_at_id continuous_const) }
+  moreover have "{x. x - a \<in> s} = op + a ` s" by force
   ultimately show ?thesis using continuous_open_preimage_univ[of "\<lambda>x. x - a" s] using assms by auto
 qed
 
@@ -3838,53 +3909,6 @@
   thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
 qed
 
-text {* We can now extend limit compositions to consider the scalar multiplier. *}
-
-lemma continuous_vmul:
-  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
-  unfolding continuous_def by (intro tendsto_intros)
-
-lemma continuous_mul:
-  fixes c :: "'a::metric_space \<Rightarrow> real"
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net c \<Longrightarrow> continuous net f
-             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
-  unfolding continuous_def by (intro tendsto_intros)
-
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
-  continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-
-lemmas continuous_on_intros = continuous_on_add continuous_on_const
-  continuous_on_id continuous_on_compose continuous_on_minus
-  continuous_on_diff continuous_on_scaleR continuous_on_mult
-  continuous_on_inner continuous_on_euclidean_component
-  uniformly_continuous_on_add uniformly_continuous_on_const
-  uniformly_continuous_on_id uniformly_continuous_on_compose
-  uniformly_continuous_on_cmul uniformly_continuous_on_neg
-  uniformly_continuous_on_sub
-
-text {* And so we have continuity of inverse. *}
-
-lemma continuous_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
-           ==> continuous net (inverse o f)"
-  unfolding continuous_def using Lim_inv by auto
-
-lemma continuous_at_within_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  assumes "continuous (at a within s) f" "f a \<noteq> 0"
-  shows "continuous (at a within s) (inverse o f)"
-  using assms unfolding continuous_within o_def
-  by (intro tendsto_intros)
-
-lemma continuous_at_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
-         ==> continuous (at a) (inverse o f) "
-  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
-
 text {* Topological properties of linear functions. *}
 
 lemma linear_lim_0:
@@ -3999,7 +4023,7 @@
 
 text{* Continuity of inverse function on compact domain. *}
 
-lemma continuous_on_inverse:
+lemma continuous_on_inv:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
     (* TODO: can this be generalized more? *)
   assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
@@ -4090,17 +4114,6 @@
   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))"
   unfolding continuous_on_iff dist_norm by simp
 
-lemma continuous_at_norm: "continuous (at x) norm"
-  unfolding continuous_at by (intro tendsto_intros)
-
-lemma continuous_on_norm: "continuous_on s norm"
-unfolding continuous_on by (intro ballI tendsto_intros)
-
-lemma continuous_at_infnorm: "continuous (at x) infnorm"
-  unfolding continuous_at Lim_at o_def unfolding dist_norm
-  apply auto apply (rule_tac x=e in exI) apply auto
-  using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
-
 text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
 
 lemma compact_attains_sup:
@@ -5219,7 +5232,7 @@
 
 lemma homeomorphism_compact:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
-    (* class constraint due to continuous_on_inverse *)
+    (* class constraint due to continuous_on_inv *)
   assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
   shows "\<exists>g. homeomorphism s t f g"
 proof-
@@ -5242,12 +5255,12 @@
   hence "g ` t = s" by auto
   ultimately
   show ?thesis unfolding homeomorphism_def homeomorphic_def
-    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
+    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
 qed
 
 lemma homeomorphic_compact:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
-    (* class constraint due to continuous_on_inverse *)
+    (* class constraint due to continuous_on_inv *)
   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
           \<Longrightarrow> s homeomorphic t"
   unfolding homeomorphic_def by (metis homeomorphism_compact)