# HG changeset patch # User huffman # Date 1381160390 25200 # Node ID 1a13325269c24a22859529aea7f84a1fdb6d863f # Parent 3fd3b1683d2bd0b4c525e449ad981963dfcc1568 new topological lemmas; tuned proofs diff -r 3fd3b1683d2b -r 1a13325269c2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Oct 06 20:54:28 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Oct 07 08:39:50 2013 -0700 @@ -789,18 +789,20 @@ "a - b \ c \ a \ c + b" by arith+ -lemma open_ball[intro, simp]: "open (ball x e)" - unfolding open_dist ball_def mem_Collect_eq Ball_def - unfolding dist_commute - apply clarify - apply (rule_tac x="e - dist xa x" in exI) - using dist_triangle_alt[where z=x] - apply (clarsimp simp add: diff_less_iff) - apply atomize - apply (erule_tac x="y" in allE) - apply (erule_tac x="xa" in allE) - apply arith - done +lemma open_vimage: (* TODO: move to Topological_Spaces.thy *) + assumes "open s" and "continuous_on UNIV f" + shows "open (vimage f s)" + using assms unfolding continuous_on_open_vimage [OF open_UNIV] + by simp + +lemma open_ball [intro, simp]: "open (ball x e)" +proof - + have "open (dist x -` {.. (\x\S. \e>0. ball x e \ S)" unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. @@ -1889,7 +1891,6 @@ lemma closed_sequential_limits: fixes S :: "'a::first_countable_topology set" shows "closed S \ (\x l. (\n. x n \ S) \ (x ---> l) sequentially \ l \ S)" - unfolding closed_limpt using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a] by metis @@ -2129,15 +2130,20 @@ subsection {* More properties of closed balls *} +lemma closed_vimage: (* TODO: move to Topological_Spaces.thy *) + assumes "closed s" and "continuous_on UNIV f" + shows "closed (vimage f s)" + using assms unfolding continuous_on_closed_vimage [OF closed_UNIV] + by simp + lemma closed_cball: "closed (cball x e)" - unfolding cball_def closed_def - unfolding Collect_neg_eq [symmetric] not_le - apply (clarsimp simp add: open_dist, rename_tac y) - apply (rule_tac x="dist x y - e" in exI, clarsimp) - apply (rename_tac x') - apply (cut_tac x=x and y=x' and z=y in dist_triangle) - apply simp - done +proof - + have "closed (dist x -` {..e})" + by (intro closed_vimage closed_atMost continuous_on_intros) + also have "dist x -` {..e} = cball x e" + by auto + finally show ?thesis . +qed lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" proof - @@ -3298,6 +3304,50 @@ where "seq_compact S \ (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f \ r) ---> l) sequentially))" +lemma seq_compactI: + assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f \ r) ---> l) sequentially" + shows "seq_compact S" + unfolding seq_compact_def using assms by fast + +lemma seq_compactE: + assumes "seq_compact S" "\n. f n \ S" + obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" + using assms unfolding seq_compact_def by fast + +lemma closed_sequentially: (* TODO: move upwards *) + assumes "closed s" and "\n. f n \ s" and "f ----> l" + shows "l \ s" +proof (rule ccontr) + assume "l \ s" + with `closed s` and `f ----> l` have "eventually (\n. f n \ - s) sequentially" + by (fast intro: topological_tendstoD) + with `\n. f n \ s` show "False" + by simp +qed + +lemma seq_compact_inter_closed: + assumes "seq_compact s" and "closed t" + shows "seq_compact (s \ t)" +proof (rule seq_compactI) + fix f assume "\n::nat. f n \ s \ t" + hence "\n. f n \ s" and "\n. f n \ t" + by simp_all + from `seq_compact s` and `\n. f n \ s` + obtain l r where "l \ s" and r: "subseq r" and l: "(f \ r) ----> l" + by (rule seq_compactE) + from `\n. f n \ t` have "\n. (f \ r) n \ t" + by simp + from `closed t` and this and l have "l \ t" + by (rule closed_sequentially) + with `l \ s` and r and l show "\l\s \ t. \r. subseq r \ (f \ r) ----> l" + by fast +qed + +lemma seq_compact_closed_subset: + assumes "closed s" and "s \ t" and "seq_compact t" + shows "seq_compact s" + using assms seq_compact_inter_closed [of t s] by (simp add: Int_absorb1) + lemma seq_compact_imp_countably_compact: fixes U :: "'a :: first_countable_topology set" assumes "seq_compact U" @@ -3410,16 +3460,6 @@ using `x \ U` by (auto simp: convergent_def comp_def) qed -lemma seq_compactI: - assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f \ r) ---> l) sequentially" - shows "seq_compact S" - unfolding seq_compact_def using assms by fast - -lemma seq_compactE: - assumes "seq_compact S" "\n. f n \ S" - obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" - using assms unfolding seq_compact_def by fast - lemma countably_compact_imp_acc_point: assumes "countably_compact s" and "countable t" @@ -3654,6 +3694,8 @@ "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s" using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass . +subsection {* Metric spaces with the Heine-Borel property *} + text {* A metric space (or topological vector space) is said to have the Heine-Borel property if every closed and bounded subset is compact. @@ -3678,7 +3720,7 @@ from f have fr: "\n. (f \ r) n \ s" by simp have "l \ s" using `closed s` fr l - unfolding closed_sequential_limits by blast + by (rule closed_sequentially) show "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" using `l \ s` r l by blast qed @@ -3859,11 +3901,21 @@ using l r by fast qed -subsubsection{* Completeness *} +subsubsection {* Completeness *} definition complete :: "'a::metric_space set \ bool" where "complete s \ (\f. (\n. f n \ s) \ Cauchy f \ (\l\s. f ----> l))" +lemma completeI: + assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f ----> l" + shows "complete s" + using assms unfolding complete_def by fast + +lemma completeE: + assumes "complete s" and "\n. f n \ s" and "Cauchy f" + obtains l where "l \ s" and "f ----> l" + using assms unfolding complete_def by fast + lemma compact_imp_complete: assumes "compact s" shows "complete s" @@ -4085,49 +4137,57 @@ instance euclidean_space \ banach .. -lemma complete_univ: "complete (UNIV :: 'a::complete_space set)" -proof (simp add: complete_def, rule, rule) - fix f :: "nat \ 'a" - assume "Cauchy f" +lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)" +proof (rule completeI) + fix f :: "nat \ 'a" assume "Cauchy f" then have "convergent f" by (rule Cauchy_convergent) - then show "\l. f ----> l" unfolding convergent_def . + then show "\l\UNIV. f ----> l" unfolding convergent_def by simp qed lemma complete_imp_closed: assumes "complete s" shows "closed s" -proof - - { - fix x - assume "x islimpt s" - then obtain f where f: "\n. f n \ s - {x}" "(f ---> x) sequentially" - unfolding islimpt_sequential by auto - then obtain l where l: "l\s" "(f ---> l) sequentially" - using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto - then have "x \ s" - using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto - } - then show "closed s" unfolding closed_limpt by auto -qed +proof (unfold closed_sequential_limits, clarify) + fix f x assume "\n. f n \ s" and "f ----> x" + from `f ----> x` have "Cauchy f" + by (rule LIMSEQ_imp_Cauchy) + with `complete s` and `\n. f n \ s` obtain l where "l \ s" and "f ----> l" + by (rule completeE) + from `f ----> x` and `f ----> l` have "x = l" + by (rule LIMSEQ_unique) + with `l \ s` show "x \ s" + by simp +qed + +lemma complete_inter_closed: + assumes "complete s" and "closed t" + shows "complete (s \ t)" +proof (rule completeI) + fix f assume "\n. f n \ s \ t" and "Cauchy f" + then have "\n. f n \ s" and "\n. f n \ t" + by simp_all + from `complete s` obtain l where "l \ s" and "f ----> l" + using `\n. f n \ s` and `Cauchy f` by (rule completeE) + from `closed t` and `\n. f n \ t` and `f ----> l` have "l \ t" + by (rule closed_sequentially) + with `l \ s` and `f ----> l` show "\l\s \ t. f ----> l" + by fast +qed + +lemma complete_closed_subset: + assumes "closed s" and "s \ t" and "complete t" + shows "complete s" + using assms complete_inter_closed [of t s] by (simp add: Int_absorb1) lemma complete_eq_closed: - fixes s :: "'a::complete_space set" - shows "complete s \ closed s" (is "?lhs = ?rhs") + fixes s :: "('a::complete_space) set" + shows "complete s \ closed s" proof - assume ?lhs - then show ?rhs by (rule complete_imp_closed) + assume "closed s" then show "complete s" + using subset_UNIV complete_UNIV by (rule complete_closed_subset) next - assume ?rhs - { - fix f - assume as:"\n::nat. f n \ s" "Cauchy f" - then obtain l where "(f ---> l) sequentially" - using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto - then have "\l\s. (f ---> l) sequentially" - using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] - using as(1) by auto - } - then show ?lhs unfolding complete_def by auto + assume "complete s" then show "closed s" + by (rule complete_imp_closed) qed lemma convergent_eq_cauchy: @@ -4142,13 +4202,13 @@ lemma compact_cball[simp]: fixes x :: "'a::heine_borel" - shows "compact(cball x e)" + shows "compact (cball x e)" using compact_eq_bounded_closed bounded_cball closed_cball by blast lemma compact_frontier_bounded[intro]: fixes s :: "'a::heine_borel set" - shows "bounded s \ compact(frontier s)" + shows "bounded s \ compact (frontier s)" unfolding frontier_def using compact_eq_bounded_closed by blast @@ -4168,68 +4228,51 @@ subsection {* Bounded closed nest property (proof does not use Heine-Borel) *} lemma bounded_closed_nest: - assumes "\n. closed(s n)" - and "\n. (s n \ {})" - and "(\m n. m \ n --> s n \ s m)" - and "bounded(s 0)" - shows "\a::'a::heine_borel. \n::nat. a \ s(n)" + fixes s :: "nat \ ('a::heine_borel) set" + assumes "\n. closed (s n)" + and "\n. s n \ {}" + and "\m n. m \ n \ s n \ s m" + and "bounded (s 0)" + shows "\a. \n. a \ s n" proof - - from assms(2) obtain x where x:"\n::nat. x n \ s n" - using choice[of "\n x. x\ s n"] by auto - from assms(4,1) have *:"seq_compact (s 0)" - using bounded_closed_imp_seq_compact[of "s 0"] by auto - - then obtain l r where lr:"l\s 0" "subseq r" "((x \ r) ---> l) sequentially" - unfolding seq_compact_def - apply (erule_tac x=x in allE) - using x using assms(3) - apply blast - done - - { + from assms(2) obtain x where x: "\n. x n \ s n" + using choice[of "\n x. x \ s n"] by auto + from assms(4,1) have "seq_compact (s 0)" + by (simp add: bounded_closed_imp_seq_compact) + then obtain l r where lr: "l \ s 0" "subseq r" "(x \ r) ----> l" + using x and assms(3) unfolding seq_compact_def by blast + have "\n. l \ s n" + proof fix n :: nat - { - fix e :: real - assume "e>0" - with lr(3) obtain N where N:"\m\N. dist ((x \ r) m) l < e" - unfolding LIMSEQ_def by auto - then have "dist ((x \ r) (max N n)) l < e" by auto - moreover - have "r (max N n) \ n" using lr(2) using seq_suble[of r "max N n"] - by auto - then have "(x \ r) (max N n) \ s n" - using x - apply (erule_tac x=n in allE) - using x - apply (erule_tac x="r (max N n)" in allE) - using assms(3) - apply (erule_tac x=n in allE) - apply (erule_tac x="r (max N n)" in allE) - apply auto - done - ultimately have "\y\s n. dist y l < e" - by auto - } - then have "l \ s n" - using closed_approachable[of "s n" l] assms(1) by blast - } - then show ?thesis by auto + have "closed (s n)" + using assms(1) by simp + moreover have "\i. (x \ r) i \ s i" + using x and assms(3) and lr(2) [THEN seq_suble] by auto + then have "\i. (x \ r) (i + n) \ s n" + using assms(3) by (fast intro!: le_add2) + moreover have "(\i. (x \ r) (i + n)) ----> l" + using lr(3) by (rule LIMSEQ_ignore_initial_segment) + ultimately show "l \ s n" + by (rule closed_sequentially) + qed + then show ?thesis .. qed text {* Decreasing case does not even need compactness, just completeness. *} lemma decreasing_closed_nest: + fixes s :: "nat \ ('a::complete_space) set" assumes - "\n. closed(s n)" - "\n. (s n \ {})" - "\m n. m \ n --> s n \ s m" - "\e>0. \n. \x \ (s n). \ y \ (s n). dist x y < e" - shows "\a::'a::complete_space. \n::nat. a \ s n" -proof- - have "\n. \ x. x\s n" + "\n. closed (s n)" + "\n. s n \ {}" + "\m n. m \ n \ s n \ s m" + "\e>0. \n. \x\s n. \y\s n. dist x y < e" + shows "\a. \n. a \ s n" +proof - + have "\n. \x. x \ s n" using assms(2) by auto then have "\t. \n. t n \ s n" - using choice[of "\ n x. x \ s n"] by auto + using choice[of "\n x. x \ s n"] by auto then obtain t where t: "\n. t n \ s n" by auto { fix e :: real @@ -4250,7 +4293,7 @@ then have "Cauchy t" unfolding cauchy_def by auto then obtain l where l:"(t ---> l) sequentially" - using complete_univ unfolding complete_def by auto + using complete_UNIV unfolding complete_def by auto { fix n :: nat { @@ -4285,7 +4328,7 @@ assumes "\n. closed(s n)" "\n. s n \ {}" - "\m n. m \ n --> s n \ s m" + "\m n. m \ n \ s n \ s m" "\e>0. \n. \x \ (s n). \ y\(s n). dist x y < e" shows "\a. \(range s) = {a}" proof - @@ -7350,14 +7393,14 @@ fix y assume "a \ y" "y \ b" "m > 0" then have "m *\<^sub>R a + c \ m *\<^sub>R y + c" and "m *\<^sub>R y + c \ m *\<^sub>R b + c" - unfolding eucl_le[where 'a='a] by (auto simp: inner_simps) + unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib) } moreover { fix y assume "a \ y" "y \ b" "m < 0" then have "m *\<^sub>R b + c \ m *\<^sub>R y + c" and "m *\<^sub>R y + c \ m *\<^sub>R a + c" - unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_simps) + unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib) } moreover { @@ -7366,7 +7409,7 @@ then have "y \ (\x. m *\<^sub>R x + c) ` {a..b}" unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) - apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_simps) + apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) done } moreover @@ -7376,7 +7419,7 @@ then have "y \ (\x. m *\<^sub>R x + c) ` {a..b}" unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) - apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_simps) + apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) done } ultimately show ?thesis using False by auto