author huffman Thu, 20 Mar 2014 09:21:39 -0700 changeset 56226 29fd6bd9228e parent 56225 00112abe9b25 child 56227 67a5f004583d child 56235 083b41092afe
generalize some theorems
```--- 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)"```
```--- 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)"```