# HG changeset patch # User huffman # Date 1244515524 25200 # Node ID f5bde0d3c3857b9fdb4c809b5608a8e610c7c157 # Parent 0de814d2ff959721b5b6e69be8cb0d28237c0b8d generalize compact/closure lemmas diff -r 0de814d2ff95 -r f5bde0d3c385 src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 19:18:47 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 19:45:24 2009 -0700 @@ -3941,11 +3941,18 @@ thus ?thesis unfolding Lim_at by auto qed +lemma bounded_linear_continuous_at: + assumes "bounded_linear f" shows "continuous (at a) f" + unfolding continuous_at using assms + apply (rule bounded_linear.tendsto) + apply (rule Lim_at_id [unfolded id_def]) + done + lemma linear_continuous_at: fixes f :: "real ^ _ \ real ^ _" assumes "linear f" shows "continuous (at a) f" - unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms] - unfolding Lim_null[of "\x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto + using assms unfolding linear_conv_bounded_linear + by (rule bounded_linear_continuous_at) lemma linear_continuous_within: fixes f :: "real ^ _ \ real ^ _" @@ -4276,24 +4283,25 @@ text{* Hence some useful properties follow quite easily. *} +lemma compact_scaleR_image: + fixes s :: "'a::real_normed_vector set" + assumes "compact s" shows "compact ((\x. scaleR c 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 *s x) ` s)" -proof- - let ?f = "\x. c *s x" - have *:"linear ?f" unfolding linear_def vector_smult_assoc vector_add_ldistrib real_mult_commute by auto - show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] - using linear_continuous_at[OF *] assms by auto -qed + using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image) lemma compact_negations: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. -x) ` s)" -proof- - have "(\x. - x) ` s = (\x. (- 1) *s x) ` s" - unfolding vector_sneg_minus1 .. - thus ?thesis using compact_scaling[OF assms, of "-1"] by auto -qed + using compact_scaleR_image [OF assms, of "- 1"] by auto lemma compact_sums: fixes s t :: "(real ^ _) set" @@ -4401,9 +4409,9 @@ text{* Related results with closure as the conclusion. *} -lemma closed_scaling: - fixes s :: "(real ^ _) set" - assumes "closed s" shows "closed ((\x. c *s x) ` s)" +lemma closed_scaleR_image: + fixes s :: "'a::real_normed_vector set" + assumes "closed s" shows "closed ((\x. scaleR c x) ` s)" proof(cases "s={}") case True thus ?thesis by auto next @@ -4414,29 +4422,39 @@ case True thus ?thesis apply auto unfolding * using closed_sing by auto next case False - { fix x l assume as:"\n::nat. x n \ op *s c ` s" "(x ---> l) sequentially" - { fix n::nat have "(1 / c) *s x n \ s" using as(1)[THEN spec[where x=n]] using `c\0` by (auto simp add: vector_smult_assoc) } + { fix x l assume as:"\n::nat. x n \ scaleR c ` s" "(x ---> l) sequentially" + { fix n::nat have "scaleR (1 / c) (x n) \ s" + using as(1)[THEN spec[where x=n]] + using `c\0` by (auto simp add: vector_smult_assoc) + } moreover { fix e::real assume "e>0" hence "0 < e *\c\" using `c\0` mult_pos_pos[of e "abs c"] by auto - then obtain N where "\n\N. dist (x n) l < e * \c\" using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto - hence "\N. \n\N. dist ((1 / c) *s x n) ((1 / c) *s l) < e" unfolding dist_norm unfolding vector_ssub_ldistrib[THEN sym] norm_mul + then obtain N where "\n\N. dist (x n) l < e * \c\" + using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto + hence "\N. \n\N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e" + unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR using mult_imp_div_pos_less[of "abs c" _ e] `c\0` by auto } - hence "((\n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto - ultimately have "l \ op *s c ` s" using assms[unfolded closed_sequential_limits, THEN spec[where x="\n. (1/c) *s x n"], THEN spec[where x="(1/c) *s l"]] - unfolding image_iff using `c\0` apply(rule_tac x="(1 / c) *s l" in bexI) apply auto unfolding vector_smult_assoc by auto } - thus ?thesis unfolding closed_sequential_limits by auto + hence "((\n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto + ultimately have "l \ scaleR c ` s" + using assms[unfolded closed_sequential_limits, THEN spec[where x="\n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]] + unfolding image_iff using `c\0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto } + thus ?thesis unfolding closed_sequential_limits by fast qed qed +lemma closed_scaling: + fixes s :: "(real ^ _) set" + assumes "closed s" shows "closed ((\x. c *s x) ` s)" + using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image) + lemma closed_negations: - fixes s :: "(real ^ _) set" (* FIXME: generalize *) + fixes s :: "'a::real_normed_vector set" assumes "closed s" shows "closed ((\x. -x) ` s)" - using closed_scaling[OF assms, of "- 1"] - unfolding vector_sneg_minus1 by auto + using closed_scaleR_image[OF assms, of "- 1"] by simp lemma compact_closed_sums: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" "closed t" shows "closed {x + y | x y. x \ s \ y \ t}" proof- let ?S = "{x + y |x y. x \ s \ y \ t}" @@ -4452,11 +4470,11 @@ using f(3) by auto hence "l \ ?S" using `l' \ s` apply auto apply(rule_tac x=l' in exI) apply(rule_tac x="l - l'" in exI) by auto } - thus ?thesis unfolding closed_sequential_limits by auto + thus ?thesis unfolding closed_sequential_limits by fast qed lemma closed_compact_sums: - fixes s t :: "(real ^ _) set" + fixes s t :: "'a::real_normed_vector set" assumes "closed s" "compact t" shows "closed {x + y | x y. x \ s \ y \ t}" proof- @@ -4466,7 +4484,7 @@ qed lemma compact_closed_differences: - fixes s t :: "(real ^ _) set" + fixes s t :: "'a::real_normed_vector set" assumes "compact s" "closed t" shows "closed {x - y | x y. x \ s \ y \ t}" proof- @@ -4476,7 +4494,7 @@ qed lemma closed_compact_differences: - fixes s t :: "(real ^ _) set" + fixes s t :: "'a::real_normed_vector set" assumes "closed s" "compact t" shows "closed {x - y | x y. x \ s \ y \ t}" proof- @@ -4486,7 +4504,7 @@ qed lemma closed_translation: - fixes s :: "(real ^ _) set" (* FIXME: generalize *) + fixes a :: "'a::real_normed_vector" assumes "closed s" shows "closed ((\x. a + x) ` s)" proof- have "{a + y |y. y \ s} = (op + a ` s)" by auto @@ -4494,21 +4512,26 @@ qed lemma translation_UNIV: - "range (\x::real^'a. a + x) = UNIV" + fixes a :: "'a::ab_group_add" shows "range (\x. a + x) = UNIV" apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto -lemma translation_diff: "(\x::real^'a. a + x) ` (s - t) = ((\x. a + x) ` s) - ((\x. a + x) ` t)" by auto +lemma translation_diff: + fixes a :: "'a::ab_group_add" + shows "(\x. a + x) ` (s - t) = ((\x. a + x) ` s) - ((\x. a + x) ` t)" + by auto lemma closure_translation: - fixes s :: "(real ^ _) set" (* FIXME: generalize *) + fixes a :: "'a::real_normed_vector" shows "closure ((\x. a + x) ` s) = (\x. a + x) ` (closure s)" proof- - have *:"op + a ` (UNIV - s) = UNIV - op + a ` s" apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto - show ?thesis unfolding closure_interior translation_diff translation_UNIV using interior_translation[of a "UNIV - s"] unfolding * by auto + have *:"op + a ` (UNIV - s) = UNIV - op + a ` s" + apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto + show ?thesis unfolding closure_interior translation_diff translation_UNIV + using interior_translation[of a "UNIV - s"] unfolding * by auto qed lemma frontier_translation: - fixes s :: "(real ^ _) set" (* FIXME: generalize *) + fixes a :: "'a::real_normed_vector" shows "frontier((\x. a + x) ` s) = (\x. a + x) ` (frontier s)" unfolding frontier_def translation_diff interior_translation closure_translation by auto