src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

   unfolding closure_open_interval[OF assms, THEN sym] unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
 
 (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
 
-lemma closed_interval_left: fixes b::"'a::ordered_euclidean_space"
+lemma closed_interval_left: fixes b::"'a::euclidean_space"
   shows "closed {x::'a. \<forall>i<DIM('a). x$$i \<le> b$$i}"
 proof-
   { fix i assume i:"i<DIM('a)"
     fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i<DIM('a). x $$ i \<le> b $$ i}. x' \<noteq> x \<and> dist x' x < e"
     { assume "x$$i > b$$i"

         by auto   }
     hence "x$$i \<le> b$$i" by(rule ccontr)auto  }
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-lemma closed_interval_right: fixes a::"'a::ordered_euclidean_space"
+lemma closed_interval_right: fixes a::"'a::euclidean_space"
   shows "closed {x::'a. \<forall>i<DIM('a). a$$i \<le> x$$i}"
 proof-
   { fix i assume i:"i<DIM('a)"
     fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i<DIM('a). a $$ i \<le> x $$ i}. x' \<noteq> x \<and> dist x' x < e"
     { assume "a$$i > x$$i"

   have "{x. inner a x = b} = {x. inner a x \<ge> b} \<inter> {x. inner a x \<le> b}" by auto
   thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
 qed
 
 lemma closed_halfspace_component_le:
-  shows "closed {x::'a::ordered_euclidean_space. x$$i \<le> a}"
+  shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
   using closed_halfspace_le[of "(basis i)::'a" a] unfolding euclidean_component_def .
 
 lemma closed_halfspace_component_ge:
-  shows "closed {x::'a::ordered_euclidean_space. x$$i \<ge> a}"
+  shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
   using closed_halfspace_ge[of a "(basis i)::'a"] unfolding euclidean_component_def .
 
 text{* Openness of halfspaces.                                                   *}
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"

   have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
   thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
 qed
 
 lemma open_halfspace_component_lt:
-  shows "open {x::'a::ordered_euclidean_space. x$$i < a}"
+  shows "open {x::'a::euclidean_space. x$$i < a}"
   using open_halfspace_lt[of "(basis i)::'a" a] unfolding euclidean_component_def .
 
 lemma open_halfspace_component_gt:
-  shows "open {x::'a::ordered_euclidean_space. x$$i  > a}"
+  shows "open {x::'a::euclidean_space. x$$i  > a}"
   using open_halfspace_gt[of a "(basis i)::'a"] unfolding euclidean_component_def .
 
 text{* This gives a simple derivation of limit component bounds.                 *}
 
-lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$$i \<le> b) net"
   shows "l$$i \<le> b"
 proof-
   { fix x have "x \<in> {x::'b. inner (basis i) x \<le> b} \<longleftrightarrow> x$$i \<le> b"
       unfolding euclidean_component_def by auto  } note * = this
   show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<le> b}" f net l] unfolding *
     using closed_halfspace_le[of "(basis i)::'b" b] and assms(1,2,3) by auto
 qed
 
-lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)$$i) net"
   shows "b \<le> l$$i"
 proof-
   { fix x have "x \<in> {x::'b. inner (basis i) x \<ge> b} \<longleftrightarrow> x$$i \<ge> b"
       unfolding euclidean_component_def by auto  } note * = this
   show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<ge> b}" f net l] unfolding *
     using closed_halfspace_ge[of b "(basis i)"] and assms(1,2,3) by auto
 qed
 
-lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
   assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$$i = b) net"
   shows "l$$i = b"
   using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
 text{* Limits relative to a union.                                               *}
 

   moreover have "?A \<inter> ?B = {}" by auto
   moreover have "s \<subseteq> ?A \<union> ?B" using as by auto
   ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto
 qed
 
-lemma connected_ivt_component: fixes x::"'a::ordered_euclidean_space" shows
+lemma connected_ivt_component: fixes x::"'a::euclidean_space" shows
  "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$$k \<le> a \<Longrightarrow> a \<le> y$$k \<Longrightarrow> (\<exists>z\<in>s.  z$$k = a)"
   using connected_ivt_hyperplane[of s x y "(basis k)::'a" a]
   unfolding euclidean_component_def by auto
 
 subsection {* Homeomorphisms *}