# HG changeset patch # User huffman # Date 1244923810 25200 # Node ID f5ffe064412abcc960bee5ca080df288f8a2dd49 # Parent 1dfa55a46d7d44892a554e6a42ae0c82e27c1c58 generalize lemmas diff -r 1dfa55a46d7d -r f5ffe064412a src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 11:56:41 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Sat Jun 13 13:10:10 2009 -0700 @@ -1238,7 +1238,7 @@ text{* Basic arithmetical combining theorems for limits. *} -lemma Lim_linear: fixes f :: "('a \ real^'n::finite)" and h :: "(real^'n \ real^'m::finite)" +lemma Lim_linear: assumes "(f ---> l) net" "bounded_linear h" shows "((\x. h (f x)) ---> h l) net" using `bounded_linear h` `(f ---> l) net` @@ -1251,7 +1251,7 @@ by (rule tendsto_const) lemma Lim_cmul: - fixes f :: "'a \ real ^ 'n::finite" + fixes f :: "'a \ 'b::real_normed_vector" shows "(f ---> l) net ==> ((\x. c *\<^sub>R f x) ---> c *\<^sub>R l) net" by (intro tendsto_intros) @@ -1433,7 +1433,6 @@ text{* Limit under bilinear function *} lemma Lim_bilinear: - fixes net :: "'a net" and h:: "real ^'m::finite \ real ^'n::finite \ real ^'p::finite" assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h" shows "((\x. h (f x) (g x)) ---> (h l m)) net" using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net` @@ -2062,7 +2061,6 @@ qed lemma bounded_linear_image: - fixes f :: "real^'m::finite \ real^'n::finite" assumes "bounded S" "bounded_linear f" shows "bounded(f ` S)" proof- @@ -2078,7 +2076,7 @@ qed lemma bounded_scaling: - fixes S :: "(real ^ 'n::finite) set" + fixes S :: "'a::real_normed_vector set" shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" apply (rule bounded_linear_image, assumption) apply (rule scaleR.bounded_linear_right) @@ -3426,7 +3424,7 @@ by (auto simp add: continuous_def Lim_const) lemma continuous_cmul: - fixes f :: "'a::t2_space \ real ^ 'n::finite" + fixes f :: "'a::t2_space \ 'b::real_normed_vector" shows "continuous net f ==> continuous net (\x. c *\<^sub>R f x)" by (auto simp add: continuous_def Lim_cmul) @@ -3452,7 +3450,7 @@ unfolding continuous_on_eq_continuous_within using continuous_const by blast lemma continuous_on_cmul: - fixes f :: "'a::metric_space \ real ^ _" + fixes f :: "'a::metric_space \ 'b::real_normed_vector" shows "continuous_on s f ==> continuous_on s (\x. c *\<^sub>R (f x))" unfolding continuous_on_eq_continuous_within using continuous_cmul by blast @@ -3480,7 +3478,8 @@ unfolding uniformly_continuous_on_def by simp lemma uniformly_continuous_on_cmul: - fixes f :: "'a::real_normed_vector \ real ^ _" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" + (* FIXME: generalize 'a to metric_space *) assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" proof- @@ -3869,7 +3868,7 @@ qed lemma open_affinity: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "open s" "c \ 0" shows "open ((\x. a + c *\<^sub>R x) ` s)" proof- @@ -4021,7 +4020,7 @@ subsection{* Topological properties of linear functions. *} -lemma linear_lim_0: fixes f::"real^'a::finite \ real^'b::finite" +lemma linear_lim_0: assumes "bounded_linear f" shows "(f ---> 0) (at (0))" proof- interpret f: bounded_linear f by fact @@ -4030,44 +4029,34 @@ thus ?thesis unfolding f.zero . qed -lemma bounded_linear_continuous_at: +lemma linear_continuous_at: assumes "bounded_linear f" shows "continuous (at a) f" unfolding continuous_at using assms apply (rule bounded_linear.tendsto) apply (rule tendsto_ident_at) done -lemma linear_continuous_at: - fixes f :: "real ^ _ \ real ^ _" - assumes "bounded_linear f" shows "continuous (at a) f" - using assms by (rule bounded_linear_continuous_at) - lemma linear_continuous_within: - fixes f :: "real ^ _ \ real ^ _" shows "bounded_linear f ==> continuous (at x within s) f" using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto lemma linear_continuous_on: - fixes f :: "real ^ _ \ real ^ _" shows "bounded_linear f ==> continuous_on s f" using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto text{* Also bilinear functions, in composition form. *} lemma bilinear_continuous_at_compose: - fixes h :: "real ^ _ \ real ^ _ \ real ^ _" shows "continuous (at x) f \ continuous (at x) g \ bounded_bilinear h ==> continuous (at x) (\x. h (f x) (g x))" unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto lemma bilinear_continuous_within_compose: - fixes h :: "real ^ _ \ real ^ _ \ real ^ _" shows "continuous (at x within s) f \ continuous (at x within s) g \ bounded_bilinear h ==> continuous (at x within s) (\x. h (f x) (g x))" unfolding continuous_within using Lim_bilinear[of f "f x"] by auto lemma bilinear_continuous_on_compose: - fixes h :: "real ^ _ \ real ^ _ \ real ^ _" shows "continuous_on s f \ continuous_on s g \ bounded_bilinear h ==> continuous_on s (\x. h (f x) (g x))" unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto @@ -4224,10 +4213,10 @@ subsection{* We can now extend limit compositions to consider the scalar multiplier. *} lemma Lim_mul: - fixes f :: "'a \ real ^ _" + fixes f :: "'a \ 'b::real_normed_vector" assumes "(c ---> d) net" "(f ---> l) net" shows "((\x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net" - unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto) + using assms by (rule scaleR.tendsto) lemma Lim_vmul: fixes c :: "'a \ real" and v :: "'b::real_normed_vector" @@ -4358,25 +4347,20 @@ text{* Hence some useful properties follow quite easily. *} -lemma compact_scaleR_image: +lemma compact_scaling: fixes s :: "'a::real_normed_vector set" - assumes "compact s" shows "compact ((\x. scaleR c x) ` s)" + assumes "compact s" shows "compact ((\x. c *\<^sub>R x) ` s)" proof- let ?f = "\x. scaleR c x" have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right) show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] - using bounded_linear_continuous_at[OF *] assms by auto -qed - -lemma compact_scaling: - fixes s :: "(real ^ _) set" - assumes "compact s" shows "compact ((\x. c *\<^sub>R x) ` s)" - using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image) + using linear_continuous_at[OF *] assms by auto +qed lemma compact_negations: fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. -x) ` s)" - using compact_scaleR_image [OF assms, of "- 1"] by auto + using compact_scaling [OF assms, of "- 1"] by auto lemma compact_sums: fixes s t :: "'a::real_normed_vector set" @@ -4407,7 +4391,7 @@ qed lemma compact_affinity: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. a + c *\<^sub>R x) ` s)" proof- have "op + a ` op *\<^sub>R c ` s = (\x. a + c *\<^sub>R x) ` s" by auto @@ -4481,9 +4465,9 @@ text{* Related results with closure as the conclusion. *} -lemma closed_scaleR_image: +lemma closed_scaling: fixes s :: "'a::real_normed_vector set" - assumes "closed s" shows "closed ((\x. scaleR c x) ` s)" + assumes "closed s" shows "closed ((\x. c *\<^sub>R x) ` s)" proof(cases "s={}") case True thus ?thesis by auto next @@ -4515,15 +4499,10 @@ qed qed -lemma closed_scaling: - fixes s :: "(real ^ _) set" - assumes "closed s" shows "closed ((\x. c *\<^sub>R x) ` s)" - using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image) - lemma closed_negations: fixes s :: "'a::real_normed_vector set" assumes "closed s" shows "closed ((\x. -x) ` s)" - using closed_scaleR_image[OF assms, of "- 1"] by simp + using closed_scaling[OF assms, of "- 1"] by simp lemma compact_closed_sums: fixes s :: "'a::real_normed_vector set" @@ -5140,24 +5119,12 @@ subsection{* Closure of halfspaces and hyperplanes. *} -lemma Lim_dot: fixes f :: "real^'m \ real^'n::finite" - assumes "(f ---> l) net" shows "((\y. a \ (f y)) ---> a \ l) net" - unfolding dot_def by (intro tendsto_intros assms) - -lemma continuous_at_dot: - fixes x :: "real ^ _" - shows "continuous (at x) (\y. a \ y)" -proof- - have "((\x. x) ---> x) (at x)" unfolding Lim_at by auto - thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\x. x" x "at x" a] by auto -qed - -lemma continuous_on_dot: - fixes s :: "(real ^ _) set" - shows "continuous_on s (\y. a \ y)" - using continuous_at_imp_continuous_on[of s "\y. a \ y"] - using continuous_at_dot - by auto +lemma Lim_inner: + assumes "(f ---> l) net" shows "((\y. inner a (f y)) ---> inner a l) net" + by (intro tendsto_intros assms) + +lemma continuous_at_inner: "continuous (at x) (inner a)" + unfolding continuous_at by (intro tendsto_intros) lemma continuous_on_inner: fixes s :: "'a::real_inner set" @@ -5266,7 +5233,7 @@ using assms unfolding continuous_on unfolding Lim_within_union unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto -lemma continuous_on_cases: fixes g :: "real^'m::finite \ real ^'n::finite" +lemma continuous_on_cases: assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" "\x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x" shows "continuous_on (s \ t) (\x. if P x then f x else g x)" @@ -5322,22 +5289,24 @@ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" -definition homeomorphic :: "((real^'a::finite) set) \ ((real^'b::finite) set) \ bool" (infixr "homeomorphic" 60) where +definition + homeomorphic :: "'a::metric_space set \ 'b::metric_space set \ bool" + (infixr "homeomorphic" 60) where homeomorphic_def: "s homeomorphic t \ (\f g. homeomorphism s t f g)" lemma homeomorphic_refl: "s homeomorphic s" unfolding homeomorphic_def unfolding homeomorphism_def using continuous_on_id - apply(rule_tac x = "(\x::real^'a.x)" in exI) - apply(rule_tac x = "(\x::real^'b.x)" in exI) + apply(rule_tac x = "(\x. x)" in exI) + apply(rule_tac x = "(\x. x)" in exI) by blast lemma homeomorphic_sym: "s homeomorphic t \ t homeomorphic s" unfolding homeomorphic_def unfolding homeomorphism_def -by blast +by blast (* FIXME: slow *) lemma homeomorphic_trans: assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u" @@ -5379,7 +5348,8 @@ using assms unfolding inj_on_def inv_on_def by auto lemma homeomorphism_compact: - fixes f :: "real ^ _ \ real ^ _" + fixes f :: "'a::heine_borel \ 'b::heine_borel" + (* class constraint due to continuous_on_inverse *) assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof- @@ -5406,7 +5376,9 @@ qed lemma homeomorphic_compact: - "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s + fixes f :: "'a::heine_borel \ 'b::heine_borel" + (* class constraint due to continuous_on_inverse *) + shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by(metis homeomorphism_compact) @@ -5420,6 +5392,7 @@ text{* Results on translation, scaling etc. *} lemma homeomorphic_scaling: + fixes s :: "'a::real_normed_vector set" assumes "c \ 0" shows "s homeomorphic ((\x. c *\<^sub>R x) ` s)" unfolding homeomorphic_minimal apply(rule_tac x="\x. c *\<^sub>R x" in exI) @@ -5428,13 +5401,15 @@ using continuous_on_cmul[OF continuous_on_id] by auto lemma homeomorphic_translation: - "s homeomorphic ((\x. a + x) ` s)" + fixes s :: "'a::real_normed_vector set" + shows "s homeomorphic ((\x. a + x) ` s)" unfolding homeomorphic_minimal apply(rule_tac x="\x. a + x" in exI) apply(rule_tac x="\x. -a + x" in exI) using continuous_on_add[OF continuous_on_const continuous_on_id] by auto lemma homeomorphic_affinity: + fixes s :: "'a::real_normed_vector set" assumes "c \ 0" shows "s homeomorphic ((\x. a + c *\<^sub>R x) ` s)" proof- have *:"op + a ` op *\<^sub>R c ` s = (\x. a + c *\<^sub>R x) ` s" by auto @@ -5444,7 +5419,8 @@ using homeomorphic_translation[of "(\x. c *\<^sub>R x) ` s" a] unfolding * by auto qed -lemma homeomorphic_balls: fixes a b ::"real^'a::finite" +lemma homeomorphic_balls: + fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *) assumes "0 < d" "0 < e" shows "(ball a d) homeomorphic (ball b e)" (is ?th) "(cball a d) homeomorphic (cball b e)" (is ?cth)