src/HOL/Library/Topology_Euclidean_Space.thy

 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually P net)"
   by (auto simp add: eventually_def)
 
 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
 
-definition tendsto:: "('a \<Rightarrow> real ^'n::finite) \<Rightarrow> real ^'n \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
+definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
   tendsto_def: "(f ---> l) net  \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
 
 lemma tendstoD: "(f ---> l) net \<Longrightarrow> e>0 \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
   unfolding tendsto_def by auto
 

 qed
 
 lemma Lim_const: "((\<lambda>x. a) ---> a) net"
   by (auto simp add: Lim trivial_limit_def)
 
-lemma Lim_cmul: "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
+lemma Lim_cmul:
+  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  shows "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
   apply (rule Lim_linear[where f = f])
   apply simp
   apply (rule linear_compose_cmul)
   apply (rule linear_id[unfolded id_def])
   done
 
-lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
+lemma Lim_neg:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
   apply (simp add: Lim dist_norm  group_simps)
   apply (subst minus_diff_eq[symmetric])
   unfolding norm_minus_cancel by simp
 
-lemma Lim_add: fixes f :: "'a \<Rightarrow> real^'n::finite" shows
+lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
  "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
 proof-
   assume as:"(f ---> l) net" "(g ---> m) net"
   { fix e::real
     assume "e>0"

     qed
   }
   thus ?thesis unfolding tendsto_def by auto
 qed
 
-lemma Lim_sub: "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
+lemma Lim_sub:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
   unfolding diff_minus
   by (simp add: Lim_add Lim_neg)
 
-lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
-lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
+lemma Lim_null:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
+
+lemma Lim_null_norm:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
   by (simp add: Lim dist_norm norm_vec1)
 
 lemma Lim_null_comparison:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
   shows "(f ---> 0) net"
 proof(simp add: tendsto_def, rule+)
   fix e::real assume "0<e"
   { fix x

   apply (rule order_le_less_trans)
   apply (rule component_le_norm)
   by auto
 
 lemma Lim_transform_bound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   shows "(f ---> 0) net"
 proof(simp add: tendsto_def, rule+)
   fix e::real assume "e>0"
   { fix x
     assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
-    hence "dist (f x) 0 < e" by norm}
+    hence "dist (f x) 0 < e" by (simp add: dist_norm)}
   thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
     using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
     using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
     using assms `e>0` unfolding tendsto_def by blast
 qed

 qed
 
 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
 
 lemma Lim_norm_ubound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
   shows "norm(l) <= e"
 proof-
   obtain y where y: "\<exists>x. netord net x y"  "\<forall>x. netord net x y \<longrightarrow> norm (f x) \<le> e" using assms(1,3) unfolding eventually_def by auto
   show ?thesis

     assume "\<not> norm l \<le> e"
     then obtain z where z: "\<exists>x. netord net x z"  "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < norm l - e"
       using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="norm l - e" in allE) by auto
     obtain w where w:"netord net w z"  "netord net w y" using net[of net] using z(1) y(1) by blast
     hence "dist (f w) l < norm l - e \<and> norm (f w) <= e" using z(2) y(2) by auto
-    thus False using `\<not> norm l \<le> e` by norm
+    hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
+    hence "norm (f w - l) + norm (f w) < norm l" by simp
+    hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
+    thus False using `\<not> norm l \<le> e` by simp
   qed
 qed
 
 lemma Lim_norm_lbound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not> (trivial_limit net)"  "(f ---> l) net"  "eventually (\<lambda>x. e <= norm(f x)) net"
   shows "e \<le> norm l"
 proof-
   obtain y where y: "\<exists>x. netord net x y"  "\<forall>x. netord net x y \<longrightarrow> e \<le> norm (f x)" using assms(1,3) unfolding eventually_def by auto
   show ?thesis

     assume "\<not> e \<le> norm l"
     then obtain z where z: "\<exists>x. netord net x z"  "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < e - norm l"
       using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="e - norm l" in allE) by auto
     obtain w where w:"netord net w z"  "netord net w y" using net[of net] using z(1) y(1) by blast
     hence "dist (f w) l < e - norm l \<and> e \<le> norm (f w)" using z(2) y(2) by auto
-    thus False using `\<not> e \<le> norm l` by norm
+    hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
+    hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
+    hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
+    thus False by simp
   qed
 qed
 
 text{* Uniqueness of the limit, when nontrivial. *}
 

   hence "l = l'" using norm_ge_zero[of "l - l'"] unfolding le_less and dist_nz[of l l', unfolded dist_norm, THEN sym] by auto
   thus ?thesis using assms using Lim_sub[of f l net f l'] by simp
 qed
 
 lemma tendsto_Lim:
- "~(trivial_limit (net::('b::zero_neq_one net))) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
+  fixes f :: "'a::zero_neq_one \<Rightarrow> real ^ 'n::finite"
+  shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   unfolding Lim_def using Lim_unique[of net f] by auto
 
 text{* Limit under bilinear function (surprisingly tedious, but important) *}
 
 lemma norm_bound_lemma:

   using netlimit_within[of a UNIV]
   by (simp add: trivial_limit_at within_UNIV)
 
 text{* Transformation of limit. *}
 
-lemma Lim_transform: assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
+lemma Lim_transform:
+  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+  assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
   shows "(g ---> l) net"
 proof-
   from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\<lambda>x. f x - g x" 0 net f l] by auto
   thus "?thesis" using Lim_neg [of "\<lambda> x. - g x" "-l" net] by auto
 qed
 
-lemma Lim_transform_eventually:  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+lemma Lim_transform_eventually:
+  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+  shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   using Lim_eventually[of "\<lambda>x. f x - g x" 0 net] Lim_transform[of f g net l] by auto
 
 lemma Lim_transform_within:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   fixes x :: "real ^ 'n::finite"
   assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
           "(f ---> l) (at x within S)"
   shows   "(g ---> l) (at x within S)"
 proof-
   have "((\<lambda>x. f x - g x) ---> 0) (at x within S)" unfolding Lim_within[of "\<lambda>x. f x - g x" 0 x S] using assms(1,2) by auto
   thus ?thesis using Lim_transform[of f g "at x within S" l] using assms(3) by auto
 qed
 
-lemma Lim_transform_at: "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
+lemma Lim_transform_at:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
+  shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
   (f ---> l) (at x) ==> (g ---> l) (at x)"
   apply (subst within_UNIV[symmetric])
   using Lim_transform_within[of d UNIV x f g l]
   by (auto simp add: within_UNIV)
 
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and "(f ---> l) (at a within S)"
   shows "(g ---> l) (at a within S)"
 proof-
   have "\<forall>x'\<in>S. 0 < dist x' a \<and> dist x' a < dist a b \<longrightarrow> f x' = g x'" using assms(2)
     apply auto apply(erule_tac x=x' in ballE) by (auto simp add: dist_commute)
   thus ?thesis using Lim_transform_within[of "dist a b" S a f g l] using assms(1,3) unfolding dist_nz by auto
 qed
 
 lemma Lim_transform_away_at:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
   using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl
   by (auto simp add: within_UNIV)
 
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
 proof-
   from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
   hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)

     then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
     hence "\<exists>l\<in>s. (f ---> l) sequentially" using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] using as(1) by auto  }
   thus ?lhs unfolding complete_def by auto
 qed
 
-lemma convergent_eq_cauchy: "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
+lemma convergent_eq_cauchy:
+  fixes s :: "nat \<Rightarrow> real ^ 'n::finite"
+  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
 proof
   assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
   thus ?rhs using convergent_imp_cauchy by auto
 next
   assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto

 qed
 
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
 proof-
   { fix e::real assume "e>0"

   hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
   thus ?thesis unfolding continuous_within using Lim_transform_within[of d s x f g "g x"] using assms by blast
 qed
 
 lemma continuous_transform_at:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
 proof-
   { fix e::real assume "e>0"

 qed
 
 text{* Combination results for pointwise continuity. *}
 
 lemma continuous_const: "continuous net (\<lambda>x::'a::zero_neq_one. c)"
-  by(auto simp add: continuous_def Lim_const)
+  by (auto simp add: continuous_def Lim_const)
 
 lemma continuous_cmul:
- "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
- by(auto simp add: continuous_def Lim_cmul)
+  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  shows "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
+  by (auto simp add: continuous_def Lim_cmul)
 
 lemma continuous_neg:
- "continuous net f ==> continuous net (\<lambda>x. -(f x))"
- by(auto simp add: continuous_def Lim_neg)
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
+  by (auto simp add: continuous_def Lim_neg)
 
 lemma continuous_add:
- "continuous net f \<Longrightarrow> continuous net g
-           ==> continuous net (\<lambda>x. f x + g x)"
- by(auto simp add: continuous_def Lim_add)
+  fixes f g :: "'a \<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 Lim_add)
 
 lemma continuous_sub:
- "continuous net f \<Longrightarrow> continuous net g
-           ==> continuous net (\<lambda>x. f(x) - g(x))"
- by(auto simp add: continuous_def Lim_sub)
+  fixes f g :: "'a \<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 Lim_sub)
 
 text{* Same thing for setwise continuity. *}
 
 lemma continuous_on_const:
  "continuous_on s (\<lambda>x. c)"

   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
- "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
         ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
 
 lemma bilinear_continuous_within_compose:
- "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
         ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
 
 lemma bilinear_continuous_on_compose:
  "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bilinear h

             --> x \<in> s)"
   unfolding closed_limpt islimpt_approachable forall_vec1 apply simp
   unfolding dist_vec1 vec1_in_image_vec1 abs_minus_commute by auto
 
 lemma continuous_at_vec1_range:
- "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
+  fixes f :: "real ^ _ \<Rightarrow> real"
+  shows "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
         \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
   unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
   apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
   apply(erule_tac x=e in allE) by auto
 

 qed
 
 subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
 
 lemma Lim_mul:
+  fixes f :: "'a \<Rightarrow> real ^ _"
   assumes "((vec1 o c) ---> vec1 d) net"  "(f ---> l) net"
   shows "((\<lambda>x. c(x) *s f x) ---> (d *s l)) net"
 proof-
   have "bilinear (\<lambda>x. op *s (dest_vec1 (x::real^1)))" unfolding bilinear_def linear_def
     unfolding dest_vec1_add dest_vec1_cmul
     apply vector apply auto unfolding semiring_class.right_distrib semiring_class.left_distrib by auto
   thus ?thesis using Lim_bilinear[OF assms, of "\<lambda>x y. (dest_vec1 x) *s y"] by auto
 qed
 
 lemma Lim_vmul:
- "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
+  fixes c :: "'a \<Rightarrow> real"
+  shows "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
   using Lim_mul[of c d net "\<lambda>x. v" v] using Lim_const[of v] by auto
 
 lemma continuous_vmul:
- "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
+  fixes c :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
   unfolding continuous_def using Lim_vmul[of c] by auto
 
 lemma continuous_mul:
- "continuous net (vec1 o c) \<Longrightarrow> continuous net f
+  fixes c :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o c) \<Longrightarrow> continuous net f
              ==> continuous net (\<lambda>x. c(x) *s f x) "
   unfolding continuous_def using Lim_mul[of c] by auto
 
 lemma continuous_on_vmul:
  "continuous_on s (vec1 o c) ==> continuous_on s (\<lambda>x. c(x) *s v)"

   unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
 
 text{* And so we have continuity of inverse.                                     *}
 
 lemma Lim_inv:
+  fixes f :: "'a \<Rightarrow> real"
   assumes "((vec1 o f) ---> vec1 l) (net::'a net)"  "l \<noteq> 0"
   shows "((vec1 o inverse o f) ---> vec1(inverse l)) net"
 proof(cases "trivial_limit net")
   case True thus ?thesis unfolding tendsto_def unfolding eventually_def by auto
 next

       using y1 by auto  }
   thus ?thesis unfolding tendsto_def eventually_def by auto
 qed
 
 lemma continuous_inv:
- "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
+  fixes f :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
            ==> continuous net (vec1 o inverse o f)"
   unfolding continuous_def using Lim_inv by auto
 
 lemma continuous_at_within_inv:
+  fixes f :: "real ^ _ \<Rightarrow> real"
   assumes "continuous (at a within s) (vec1 o f)" "f a \<noteq> 0"
   shows "continuous (at a within s) (vec1 o inverse o f)"
 proof(cases "trivial_limit (at a within s)")
   case True thus ?thesis unfolding continuous_def tendsto_def eventually_def by auto
 next
   case False note cs = this
   thus ?thesis using netlimit_within[OF cs] assms(2) continuous_inv[OF assms(1)] by auto
 qed
 
 lemma continuous_at_inv:
- "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
+  fixes f :: "real ^ _ \<Rightarrow> real"
+  shows "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
          ==> continuous (at a) (vec1 o inverse o f) "
   using within_UNIV[THEN sym, of a] using continuous_at_within_inv[of a UNIV] by auto
 
 subsection{* Preservation properties for pasted sets.                                  *}