--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jul 01 09:24:04 2010 -0700
@@ -1998,7 +1998,7 @@
*)
subsection {* Another intermediate value theorem formulation. *}
-lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$$k \<le> y" "y \<le> (f b)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
@@ -2007,20 +2007,20 @@
using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
using assms by(auto intro!: imageI) qed
-lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
\<Longrightarrow> f a$$k \<le> y \<Longrightarrow> y \<le> f b$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
by(rule ivt_increasing_component_on_1)
(auto simp add: continuous_at_imp_continuous_on)
-lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
by (auto simp add:euclidean_simps)
-lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
+lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
\<Longrightarrow> f b$$k \<le> y \<Longrightarrow> y \<le> f a$$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$$k = y"
by(rule ivt_decreasing_component_on_1)
@@ -2212,6 +2212,7 @@
lemma convex_on_continuous:
assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
+ (* FIXME: generalize to euclidean_space *)
shows "continuous_on s f"
unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
note dimge1 = DIM_positive[where 'a='a]
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jul 01 09:24:04 2010 -0700
@@ -4994,7 +4994,7 @@
(* 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)"
@@ -5008,7 +5008,7 @@
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)"
@@ -5076,11 +5076,11 @@
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. *}
@@ -5098,16 +5098,16 @@
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-
@@ -5117,7 +5117,7 @@
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-
@@ -5127,7 +5127,7 @@
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
@@ -5187,7 +5187,7 @@
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