author huffman Thu, 20 Mar 2014 15:13:55 -0700 changeset 56227 67a5f004583d parent 56226 29fd6bd9228e child 56236 713ae0c9e652
generalize more theorems
```--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 15:13:55 2014 -0700
@@ -888,7 +888,7 @@
text {* In particular. *}

lemma has_derivative_zero_constant:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
assumes "convex s"
and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
shows "\<exists>c. \<forall>x\<in>s. f x = c"
@@ -914,7 +914,7 @@
qed

lemma has_derivative_zero_unique:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
assumes "convex s"
and "a \<in> s"
and "f a = c"
@@ -1184,7 +1184,7 @@
text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}

lemma sussmann_open_mapping:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
assumes "open s"
and "continuous_on s f"
and "x \<in> s"```