# HG changeset patch
# User huffman
# Date 1395332499 25200
# Node ID 29fd6bd9228e7cf554db6adcce0200f7d9bbec25
# Parent  00112abe9b256c9343ac82fa76cea7275cd78b05
generalize some theorems

diff -r 00112abe9b25 -r 29fd6bd9228e src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Mar 20 12:43:48 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Mar 20 09:21:39 2014 -0700
@@ -41,7 +41,7 @@
 qed
 
 lemma brouwer_compactness_lemma:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes "compact s"
     and "continuous_on s f"
     and "\<not> (\<exists>x\<in>s. f x = 0)"
diff -r 00112abe9b25 -r 29fd6bd9228e src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 12:43:48 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 09:21:39 2014 -0700
@@ -929,7 +929,7 @@
 subsection {* Differentiability of inverse function (most basic form) *}
 
 lemma has_derivative_inverse_basic:
-  fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_derivative f') (at (g y))"
     and "bounded_linear g'"
     and "g' \<circ> f' = id"
@@ -1075,7 +1075,7 @@
 text {* Simply rewrite that based on the domain point x. *}
 
 lemma has_derivative_inverse_basic_x:
-  fixes f :: "'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_derivative f') (at x)"
     and "bounded_linear g'"
     and "g' \<circ> f' = id"
@@ -1093,7 +1093,7 @@
 text {* This is the version in Dieudonne', assuming continuity of f and g. *}
 
 lemma has_derivative_inverse_dieudonne:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "open s"
     and "open (f ` s)"
     and "continuous_on s f"
@@ -1113,7 +1113,7 @@
 text {* Here's the simplest way of not assuming much about g. *}
 
 lemma has_derivative_inverse:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "compact s"
     and "x \<in> s"
     and "f x \<in> interior (f ` s)"