src/HOL/Multivariate_Analysis/Derivative.thy

 
 
 subsection {* Proving surjectivity via Brouwer fixpoint theorem *}
 
 lemma brouwer_surjective:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'n"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "compact t"
     and "convex t"
     and "t \<noteq> {}"
     and "continuous_on t f"
     and "\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t"

     apply auto
     done
 qed
 
 lemma brouwer_surjective_cball:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'n"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "e > 0"
     and "continuous_on (cball a e) f"
     and "\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e"
     and "x \<in> s"
   shows "\<exists>y\<in>cball a e. f y = x"

   done
 
 text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}
 
 lemma sussmann_open_mapping:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "open s"
     and "continuous_on s f"
     and "x \<in> s"
     and "(f has_derivative f') (at x)"
     and "bounded_linear g'" "f' \<circ> g' = id"

     done
   with h(1) show ?thesis by blast
 qed
 
 lemma has_derivative_inverse_strong:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'n"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "open s"
     and "x \<in> s"
     and "continuous_on s f"
     and "\<forall>x\<in>s. g (f x) = x"
     and "(f has_derivative f') (at x)"

 qed
 
 text {* A rewrite based on the other domain. *}
 
 lemma has_derivative_inverse_strong_x:
-  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'a"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes "open s"
     and "g y \<in> s"
     and "continuous_on s f"
     and "\<forall>x\<in>s. g (f x) = x"
     and "(f has_derivative f') (at (g y))"

   by simp
 
 text {* On a region. *}
 
 lemma has_derivative_inverse_on:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'n"
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   assumes "open s"
     and "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
     and "\<forall>x\<in>s. g (f x) = x"
     and "f' x \<circ> g' x = id"
     and "x \<in> s"