# HG changeset patch # User huffman # Date 1379980577 25200 # Node ID 0a62ad289c4d7ea8b58095090c32b9639db4f202 # Parent 369537953d05250c5d1b1906baed0cab0d220501 tuned proofs diff -r 369537953d05 -r 0a62ad289c4d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 24 00:21:40 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 23 16:56:17 2013 -0700 @@ -5776,59 +5776,16 @@ fixes s :: "'a::real_normed_vector set" assumes "closed s" shows "closed ((\x. c *\<^sub>R x) ` s)" -proof (cases "s = {}") - case True - then show ?thesis by auto +proof (cases "c = 0") + case True then show ?thesis + by (auto simp add: image_constant_conv) next case False - show ?thesis - proof (cases "c = 0") - have *: "(\x. 0) ` s = {0}" using `s\{}` by auto - case True - then show ?thesis - apply auto - unfolding * - apply auto - done - next - case False - { - 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 - } - moreover - { - fix e :: real - assume "e > 0" - then have "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 LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto - then have "\N. \n\N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e" - unfolding dist_norm - unfolding scaleR_right_diff_distrib[symmetric] - using mult_imp_div_pos_less[of "abs c" _ e] `c\0` by auto - } - then have "((\n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" - unfolding LIMSEQ_def 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) - apply auto - done - } - then show ?thesis - unfolding closed_sequential_limits by fast - qed + from assms have "closed ((\x. inverse c *\<^sub>R x) -` s)" + by (simp add: continuous_closed_vimage) + also have "(\x. inverse c *\<^sub>R x) -` s = (\x. c *\<^sub>R x) ` s" + using `c \ 0` by (auto elim: image_eqI [rotated]) + finally show ?thesis . qed lemma closed_negations: @@ -6576,58 +6533,6 @@ unfolding closure_open_interval[OF assms, symmetric] 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::euclidean_space" - shows "closed {x::'a. \i\Basis. x\i \ b\i}" -proof - - { - fix i :: 'a - assume i: "i \ Basis" - fix x :: "'a" - assume x: "\e>0. \x'\{x. \i\Basis. x \ i \ b \ i}. x' \ x \ dist x' x < e" - { - assume "x\i > b\i" - then obtain y where "y \ i \ b \ i" "y \ x" "dist y x < x\i - b\i" - using x[THEN spec[where x="x\i - b\i"]] using i by auto - then have False - using Basis_le_norm[OF i, of "y - x"] - unfolding dist_norm inner_simps - using i - by auto - } - then have "x\i \ b\i" by (rule ccontr)auto - } - then show ?thesis - unfolding closed_limpt unfolding islimpt_approachable by blast -qed - -lemma closed_interval_right: - fixes a :: "'a::euclidean_space" - shows "closed {x::'a. \i\Basis. a\i \ x\i}" -proof - - { - fix i :: 'a - assume i: "i \ Basis" - fix x :: "'a" - assume x: "\e>0. \x'\{x. \i\Basis. a \ i \ x \ i}. x' \ x \ dist x' x < e" - { - assume "a\i > x\i" - then obtain y where "a \ i \ y \ i" "y \ x" "dist y x < a\i - x\i" - using x[THEN spec[where x="a\i - x\i"]] i by auto - then have False - using Basis_le_norm[OF i, of "y - x"] - unfolding dist_norm inner_simps - by auto - } - then have "a\i \ x\i" by (rule ccontr) auto - } - then show ?thesis - unfolding closed_limpt unfolding islimpt_approachable by blast -qed - lemma open_box: "open (box a b)" proof - have "open (\i\Basis. (op \ i) -` {a \ i <..< b \ i})" @@ -6777,6 +6682,16 @@ lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\i \ a}" by (simp add: closed_Collect_le) +lemma closed_interval_left: + fixes b :: "'a::euclidean_space" + shows "closed {x::'a. \i\Basis. x\i \ b\i}" + by (simp add: Collect_ball_eq closed_INT closed_Collect_le) + +lemma closed_interval_right: + fixes a :: "'a::euclidean_space" + shows "closed {x::'a. \i\Basis. a\i \ x\i}" + by (simp add: Collect_ball_eq closed_INT closed_Collect_le) + text {* Openness of halfspaces. *} lemma open_halfspace_lt: "open {x. inner a x < b}" @@ -7314,58 +7229,24 @@ lemma dim_substandard: assumes d: "d \ Basis" shows "dim {x::'a::euclidean_space. \i\Basis. i \ d \ x\i = 0} = card d" (is "dim ?A = _") -proof - - let ?D = "Basis :: 'a set" - have "d \ ?A" using d by (auto simp: inner_Basis) - moreover - { - fix x::"'a" assume "x \ ?A" - then have "finite d" "x \ ?A" - using assms by (auto intro: finite_subset[OF _ finite_Basis]) - from this d have "x \ span d" - proof (induct d arbitrary: x) - case empty - then have "x = 0" - apply (rule_tac euclidean_eqI) - apply auto - done - then show ?case - using subspace_0[OF subspace_span[of "{}"]] by auto - next - case (insert k F) - then have *: "\i\Basis. i \ insert k F \ x \ i = 0" by auto - have **: "F \ insert k F" by auto - def y \ "x - (x\k) *\<^sub>R k" - have y: "x = y + (x\k) *\<^sub>R k" unfolding y_def by auto - { fix i assume i': "i \ F" "i \ Basis" - then have "y \ i = 0" unfolding y_def - using *[THEN bspec[where x=i]] insert by (auto simp: inner_simps inner_Basis) } - then have "y \ span F" using insert by auto - then have "y \ span (insert k F)" - using span_mono[of F "insert k F"] using assms by auto - moreover - have "k \ span (insert k F)" by(rule span_superset, auto) - then have "(x\k) *\<^sub>R k \ span (insert k F)" - using span_mul by auto - ultimately - have "y + (x\k) *\<^sub>R k \ span (insert k F)" - using span_add by auto - then show ?case using y by auto - qed - } - then have "?A \ span d" by auto - moreover - { - fix x - assume "x \ d" - then have "x \ ?D" using assms by auto - } - then have "independent d" - using independent_mono[OF independent_Basis, of d] and assms by auto - moreover - have "d \ ?D" unfolding subset_eq using assms by auto - ultimately show ?thesis using dim_unique[of d ?A] by auto -qed +proof (rule dim_unique) + show "d \ ?A" + using d by (auto simp: inner_Basis) + show "independent d" + using independent_mono [OF independent_Basis d] . + show "?A \ span d" + proof (clarify) + fix x assume x: "\i\Basis. i \ d \ x \ i = 0" + have "finite d" + using finite_subset [OF d finite_Basis] . + then have "(\i\d. (x \ i) *\<^sub>R i) \ span d" + by (simp add: span_setsum span_clauses) + also have "(\i\d. (x \ i) *\<^sub>R i) = (\i\Basis. (x \ i) *\<^sub>R i)" + by (rule setsum_mono_zero_cong_left [OF finite_Basis d]) (auto simp add: x) + finally show "x \ span d" + unfolding euclidean_representation . + qed +qed simp text{* Hence closure and completeness of all subspaces. *}