# HG changeset patch
# User wenzelm
# Date 1395353613 -3600
# Node ID 083b41092afe2b0c5de96fbd6058c9b210b4af2d
# Parent  29fd6bd9228e7cf554db6adcce0200f7d9bbec25# Parent  59662ce44f02977f2f07839a376275f5d0d37514
merged

diff -r 59662ce44f02 -r 083b41092afe src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Mar 20 22:40:12 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -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 59662ce44f02 -r 083b41092afe src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 22:40:12 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 23:13:33 2014 +0100
@@ -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)"