# HG changeset patch # User huffman # Date 1278001444 25200 # Node ID f69f4b079275ce259c95f778f80892d6f1e99aec # Parent 0ce59483752469c49e3e25a56c621292955f3265 generalize more lemmas from ordered_euclidean_space to euclidean_space diff -r 0ce594837524 -r f69f4b079275 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ 'a::ordered_euclidean_space" +lemma ivt_increasing_component_on_1: fixes f::"real \ 'a::euclidean_space" assumes "a \ b" "continuous_on {a .. b} f" "(f a)$$k \ y" "y \ (f b)$$k" shows "\x\{a..b}. (f x)$$k = y" proof- have "f a \ f ` {a..b}" "f b \ 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 \ 'a::ordered_euclidean_space" +lemma ivt_increasing_component_1: fixes f::"real \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f \ f a$$k \ y \ y \ f b$$k \ \x\{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 \ 'a::ordered_euclidean_space" +lemma ivt_decreasing_component_on_1: fixes f::"real \ 'a::euclidean_space" assumes "a \ b" "continuous_on {a .. b} f" "(f b)$$k \ y" "y \ (f a)$$k" shows "\x\{a..b}. (f x)$$k = y" apply(subst neg_equal_iff_equal[THEN sym]) using ivt_increasing_component_on_1[of a b "\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 \ 'a::ordered_euclidean_space" +lemma ivt_decreasing_component_1: fixes f::"real \ 'a::euclidean_space" shows "a \ b \ \x\{a .. b}. continuous (at x) f \ f b$$k \ y \ y \ f a$$k \ \x\{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] diff -r 0ce594837524 -r f69f4b079275 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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. \i b$$i}" proof- { fix i assume i:"ii x$$i}" proof- { fix i assume i:"i a}" + shows "closed {x::'a::euclidean_space. x$$i \ 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 \ a}" + shows "closed {x::'a::euclidean_space. x$$i \ 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 \ 'b::ordered_euclidean_space" +lemma Lim_component_le: fixes f :: "'a \ 'b::euclidean_space" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f(x)$$i \ b) net" shows "l$$i \ 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 \ 'b::ordered_euclidean_space" +lemma Lim_component_ge: fixes f :: "'a \ 'b::euclidean_space" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$$i) net" shows "b \ 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 \ 'b::ordered_euclidean_space" +lemma Lim_component_eq: fixes f :: "'a \ 'b::euclidean_space" assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\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 \ x \ s \ y \ s \ x$$k \ a \ a \ y$$k \ (\z\s. z$$k = a)" using connected_ivt_hyperplane[of s x y "(basis k)::'a" a] unfolding euclidean_component_def by auto