# HG changeset patch
# User huffman
# Date 1272389992 25200
# Node ID 1d7704c29af360ac22605c2c09187f050d71ad1b
# Parent  89a70297564deae5505d01b9a12cda1f0a7d248f
generalized many lemmas about continuity

diff -r 89a70297564d -r 1d7704c29af3 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 22:21:03 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 27 10:39:52 2010 -0700
@@ -1659,11 +1659,16 @@
 
 text{* Some other lemmas about sequences. *}
 
+lemma sequentially_offset:
+  assumes "eventually (\<lambda>i. P i) sequentially"
+  shows "eventually (\<lambda>i. P (i + k)) sequentially"
+  using assms unfolding eventually_sequentially by (metis trans_le_add1)
+
 lemma seq_offset:
-  fixes l :: "'a::metric_space" (* TODO: generalize *)
-  shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
-  apply (auto simp add: Lim_sequentially)
-  by (metis trans_le_add1 )
+  assumes "(f ---> l) sequentially"
+  shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
+  using assms unfolding tendsto_def
+  by clarify (rule sequentially_offset, simp)
 
 lemma seq_offset_neg:
   "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -3355,24 +3360,23 @@
   assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
 qed
 
-lemma uniformly_continuous_on_sequentially:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
-                    ((\<lambda>n. x n - y n) ---> 0) sequentially
-                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+lemma uniformly_continuous_on_sequentially':
+  "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+                    ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
+                    \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. x n - y n) ---> 0) sequentially"
+  { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially"
     { fix e::real assume "e>0"
       then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
         using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
-      obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
+      obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
       { fix n assume "n\<ge>N"
-        hence "norm (f (x n) - f (y n) - 0) < e"
+        hence "dist (f (x n)) (f (y n)) < e"
           using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
-          unfolding dist_commute and dist_norm by simp  }
-      hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e"  by auto  }
-    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto  }
+          unfolding dist_commute by simp  }
+      hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"  by auto  }
+    hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto  }
   thus ?rhs by auto
 next
   assume ?rhs
@@ -3385,21 +3389,28 @@
     def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
     have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
       unfolding x_def and y_def using fa by auto
-    have 1:"\<And>(x::'a) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
-    have 2:"\<And>(x::'b) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
     { fix e::real assume "e>0"
       then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e]   by auto
       { fix n::nat assume "n\<ge>N"
         hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto
         also have "\<dots> < e" using N by auto
         finally have "inverse (real n + 1) < e" by auto
-        hence "dist (x n - y n) 0 < e" unfolding 1 using xy0[THEN spec[where x=n]] by auto  }
-      hence "\<exists>N. \<forall>n\<ge>N. dist (x n - y n) 0 < e" by auto  }
-    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n) - f (y n)) 0 < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially by auto
-    hence False unfolding 2 using fxy and `e>0` by auto  }
+        hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto  }
+      hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto  }
+    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto
+    hence False using fxy and `e>0` by auto  }
   thus ?lhs unfolding uniformly_continuous_on_def by blast
 qed
 
+lemma uniformly_continuous_on_sequentially:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+                    ((\<lambda>n. x n - y n) ---> 0) sequentially
+                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+(* BH: maybe the previous lemma should replace this one? *)
+unfolding uniformly_continuous_on_sequentially'
+unfolding dist_norm Lim_null_norm [symmetric] ..
+
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
@@ -3497,8 +3508,7 @@
   unfolding uniformly_continuous_on_def by simp
 
 lemma uniformly_continuous_on_cmul:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-    (* FIXME: generalize 'a to metric_space *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
 proof-
@@ -3507,7 +3517,8 @@
       using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
       unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   }
-  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+    unfolding dist_norm Lim_null_norm [symmetric] by auto
 qed
 
 lemma dist_minus:
@@ -3522,7 +3533,7 @@
   unfolding uniformly_continuous_on_def dist_minus .
 
 lemma uniformly_continuous_on_add:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
   shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
 proof-
@@ -3531,11 +3542,12 @@
     hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
       using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
     hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
-  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+    unfolding dist_norm Lim_null_norm [symmetric] by auto
 qed
 
 lemma uniformly_continuous_on_sub:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   unfolding ab_diff_minus
@@ -3562,25 +3574,21 @@
 
 text{* Continuity of all kinds is preserved under composition. *}
 
+lemma continuous_within_topological:
+  "continuous (at x within s) f \<longleftrightarrow>
+    (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
+      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_within
+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:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
-  assumes "continuous (at x within s) f"   "continuous (at (f x) within f ` s) g"
+  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)"
-proof-
-  { fix e::real assume "e>0"
-    with assms(2)[unfolded continuous_within Lim_within] obtain d  where "d>0" and d:"\<forall>xa\<in>f ` s. 0 < dist xa (f x) \<and> dist xa (f x) < d \<longrightarrow> dist (g xa) (g (f x)) < e" by auto
-    from assms(1)[unfolded continuous_within Lim_within] obtain d' where "d'>0" and d':"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < d" using `d>0` by auto
-    { fix y assume as:"y\<in>s"  "0 < dist y x"  "dist y x < d'"
-      hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_commute)
-      hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by auto   }
-    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (g (f xa)) (g (f x)) < e" using `d'>0` by auto  }
-  thus ?thesis unfolding continuous_within Lim_within by auto
-qed
+using assms unfolding continuous_within_topological by simp metis
 
 lemma continuous_at_compose:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x) f"  "continuous (at (f x)) g"
   shows "continuous (at x) (g o f)"
 proof-
@@ -3606,75 +3614,55 @@
 text{* Continuity in terms of open preimages. *}
 
 lemma continuous_at_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  { fix t assume as: "open t" "f x \<in> t"
-    then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
-
-    obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
-
-    have "open (ball x d)" using open_ball by auto
-    moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
-    moreover
-    { fix x' assume "x'\<in>ball x d" hence "f x' \<in> t"
-        using e[unfolded subset_eq Ball_def mem_ball, THEN spec[where x="f x'"]]    d[THEN spec[where x=x']]
-        unfolding mem_ball apply (auto simp add: dist_commute)
-        unfolding dist_nz[THEN sym] using as(2) by auto  }
-    hence "\<forall>x'\<in>ball x d. f x' \<in> t" by auto
-    ultimately have "\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x'\<in>s. f x' \<in> t)"
-      apply(rule_tac x="ball x d" in exI) by simp  }
-  thus ?rhs by auto
-next
-  assume ?rhs
-  { fix e::real assume "e>0"
-    then obtain s where s: "open s"  "x \<in> s"  "\<forall>x'\<in>s. f x' \<in> ball (f x) e" using `?rhs`[unfolded continuous_at Lim_at, THEN spec[where x="ball (f x) e"]]
-      unfolding centre_in_ball[of "f x" e, THEN sym] by auto
-    then obtain d where "d>0" and d:"ball x d \<subseteq> s" unfolding open_contains_ball by auto
-    { fix y assume "0 < dist y x \<and> dist y x < d"
-      hence "dist (f y) (f x) < e" using d[unfolded subset_eq Ball_def mem_ball, THEN spec[where x=y]]
-        using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_commute)  }
-    hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `d>0` by auto  }
-  thus ?lhs unfolding continuous_at Lim_at by auto
-qed
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
+unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
 
 lemma continuous_on_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-   shows "continuous_on s f \<longleftrightarrow>
+  shows "continuous_on s f \<longleftrightarrow>
         (\<forall>t. openin (subtopology euclidean (f ` s)) t
             --> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  { fix t assume as:"openin (subtopology euclidean (f ` s)) t"
-    have "{x \<in> s. f x \<in> t} \<subseteq> s" using as[unfolded openin_euclidean_subtopology_iff] by auto
-    moreover
-    { fix x assume as':"x\<in>{x \<in> s. f x \<in> t}"
-      then obtain e where e: "e>0" "\<forall>x'\<in>f ` s. dist x' (f x) < e \<longrightarrow> x' \<in> t" using as[unfolded openin_euclidean_subtopology_iff, THEN conjunct2, THEN bspec[where x="f x"]] by auto
-      from this(1) obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `?lhs`[unfolded continuous_on Lim_within, THEN bspec[where x=x]] using as' by auto
-      have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto)  }
-    ultimately have "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" unfolding openin_euclidean_subtopology_iff by auto  }
-  thus ?rhs unfolding continuous_on Lim_within using openin by auto
+proof (safe)
+  fix t :: "'b set"
+  assume 1: "continuous_on s f"
+  assume 2: "openin (subtopology euclidean (f ` s)) t"
+  from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
+    unfolding openin_open by auto
+  def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
+  have "open U" unfolding U_def by (simp add: open_Union)
+  moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
+  proof (intro ballI iffI)
+    fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
+      unfolding U_def t by auto
+  next
+    fix x assume "x \<in> s" and "f x \<in> t"
+    hence "x \<in> s" and "f x \<in> B"
+      unfolding t by auto
+    with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
+      unfolding t continuous_on_topological by metis
+    then show "x \<in> U"
+      unfolding U_def by auto
+  qed
+  ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
+  then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+    unfolding openin_open by fast
 next
-  assume ?rhs
-  { fix e::real and x assume "x\<in>s" "e>0"
-    { fix xa x' assume "dist (f xa) (f x) < e" "xa \<in> s" "x' \<in> s" "dist (f xa) (f x') < e - dist (f xa) (f x)"
-      hence "dist (f x') (f x) < e" using dist_triangle[of "f x'" "f x" "f xa"]
-        by (auto simp add: dist_commute)  }
-    hence "ball (f x) e \<inter> f ` s \<subseteq> f ` s \<and> (\<forall>xa\<in>ball (f x) e \<inter> f ` s. \<exists>ea>0. \<forall>x'\<in>f ` s. dist x' xa < ea \<longrightarrow> x' \<in> ball (f x) e \<inter> f ` s)" apply auto
-      apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_commute)
-    hence "\<forall>xa\<in>{xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}. \<exists>ea>0. \<forall>x'\<in>s. dist x' xa < ea \<longrightarrow> x' \<in> {xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}"
-      using `?rhs`[unfolded openin_euclidean_subtopology_iff, THEN spec[where x="ball (f x) e \<inter> f ` s"]] by auto
-    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto using `e>0` `x\<in>s` by (auto simp add: dist_commute)  }
-  thus ?lhs unfolding continuous_on Lim_within by auto
-qed
-
-(* ------------------------------------------------------------------------- *)
-(* Similarly in terms of closed sets.                                        *)
-(* ------------------------------------------------------------------------- *)
+  assume "?rhs" show "continuous_on s f"
+  unfolding continuous_on_topological
+  proof (clarify)
+    fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
+    have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
+      unfolding openin_open using `open B` by auto
+    then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
+      using `?rhs` by fast
+    then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
+      unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
+  qed
+qed
+
+text {* Similarly in terms of closed sets. *}
 
 lemma continuous_on_closed:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<longleftrightarrow>  (\<forall>t. closedin (subtopology euclidean (f ` s)) t  --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -3699,7 +3687,6 @@
 text{* Half-global and completely global cases.                                  *}
 
 lemma continuous_open_in_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "open t"
   shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof-
@@ -3710,7 +3697,6 @@
 qed
 
 lemma continuous_closed_in_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "closed t"
   shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof-
@@ -3722,7 +3708,6 @@
 qed
 
 lemma continuous_open_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f" "open s" "open t"
   shows "open {x \<in> s. f x \<in> t}"
 proof-
@@ -3732,7 +3717,6 @@
 qed
 
 lemma continuous_closed_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f" "closed s" "closed t"
   shows "closed {x \<in> s. f x \<in> t}"
 proof-
@@ -3742,26 +3726,22 @@
 qed
 
 lemma continuous_open_preimage_univ:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
   using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_closed_preimage_univ:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_open_vimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
   unfolding vimage_def by (rule continuous_open_preimage_univ)
 
 lemma continuous_closed_vimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
   unfolding vimage_def by (rule continuous_closed_preimage_univ)
 
-lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space"
+lemma interior_image_subset:
   assumes "\<forall>x. continuous (at x) f" "inj f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
   apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
@@ -3775,17 +3755,17 @@
 text{* Equality of continuous functions on closure and related results.          *}
 
 lemma continuous_closed_in_preimage_constant:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
   using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
 
 lemma continuous_closed_preimage_constant:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
   using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
 
 lemma continuous_constant_on_closure:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   assumes "continuous_on (closure s) f"
           "\<forall>x \<in> s. f x = a"
   shows "\<forall>x \<in> (closure s). f x = a"
@@ -3793,7 +3773,6 @@
     assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset unfolding subset_eq by auto
 
 lemma image_closure_subset:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on (closure s) f"  "closed t"  "(f ` s) \<subseteq> t"
   shows "f ` (closure s) \<subseteq> t"
 proof-
@@ -3852,14 +3831,14 @@
 text{* Proving a function is constant by proving open-ness of level set.         *}
 
 lemma continuous_levelset_open_in_cases:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a}
         ==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
 unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
 
 lemma continuous_levelset_open_in:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
         (\<exists>x \<in> s. f x = a)  ==> (\<forall>x \<in> s. f x = a)"
@@ -3867,7 +3846,7 @@
 by meson
 
 lemma continuous_levelset_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   assumes "connected s"  "continuous_on s f"  "open {x \<in> s. f x = a}"  "\<exists>x \<in> s.  f x = a"
   shows "\<forall>x \<in> s. f x = a"
 using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
@@ -4033,11 +4012,10 @@
   unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
 
 lemma bilinear_continuous_on_compose:
-  fixes s :: "'a::metric_space set" (* TODO: generalize *)
   shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
              ==> continuous_on s (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
-  using bilinear_continuous_within_compose[of _ s f g h] by auto
+  unfolding continuous_on_def
+  by (fast elim: bounded_bilinear.tendsto)
 
 text {* Preservation of compactness and connectedness under continuous function.  *}
 
@@ -4058,7 +4036,6 @@
 qed
 
 lemma connected_continuous_image:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "connected s"
   shows "connected(f ` s)"
 proof-
@@ -4206,10 +4183,8 @@
 lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
 unfolding continuous_at by (intro tendsto_intros)
 
-lemma continuous_on_component:
-  fixes s :: "('a::metric_space ^ 'n) set" (* TODO: generalize *)
-  shows "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on by (intro ballI tendsto_intros)
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+unfolding continuous_on_def by (intro ballI tendsto_intros)
 
 lemma continuous_at_infnorm: "continuous (at x) infnorm"
   unfolding continuous_at Lim_at o_def unfolding dist_norm