# HG changeset patch # User huffman # Date 1312841498 25200 # Node ID 5952bd355779072b8bccc20dce1557eac7a805a1 # Parent e3a744a157d42c6e4f330ca992c4ebc510635da6 generalize more lemmas about compactness diff -r e3a744a157d4 -r 5952bd355779 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 15:03:34 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 15:11:38 2011 -0700 @@ -1,6 +1,7 @@ (* title: HOL/Library/Topology_Euclidian_Space.thy Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen + Author: Brian Huffman, Portland State University *) header {* Elementary topology in Euclidean space. *} @@ -2171,6 +2172,16 @@ (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ ((f o r) ---> l) sequentially))" +lemma compactI: + assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f o r) ---> l) sequentially" + shows "compact S" + unfolding compact_def using assms by fast + +lemma compactE: + assumes "compact S" "\n. f n \ S" + obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" + using assms unfolding compact_def by fast + text {* A metric space (or topological vector space) is said to have the Heine-Borel property if every closed and bounded subset is compact. @@ -3019,56 +3030,82 @@ unfolding compact_def by simp -(* TODO: can any of the next 3 lemmas be generalized to metric spaces? *) - - (* FIXME : Rename *) -lemma compact_union[intro]: - fixes s t :: "'a::heine_borel set" - shows "compact s \ compact t ==> compact (s \ t)" - unfolding compact_eq_bounded_closed - using bounded_Un[of s t] - using closed_Un[of s t] - by simp - -lemma compact_inter[intro]: - fixes s t :: "'a::heine_borel set" - shows "compact s \ compact t ==> compact (s \ t)" - unfolding compact_eq_bounded_closed - using bounded_Int[of s t] - using closed_Int[of s t] - by simp - -lemma compact_inter_closed[intro]: - fixes s t :: "'a::heine_borel set" - shows "compact s \ closed t ==> compact (s \ t)" - unfolding compact_eq_bounded_closed - using closed_Int[of s t] - using bounded_subset[of "s \ t" s] - by blast - -lemma closed_inter_compact[intro]: - fixes s t :: "'a::heine_borel set" - shows "closed s \ compact t ==> compact (s \ t)" -proof- - assume "closed s" "compact t" +lemma subseq_o: "subseq r \ subseq s \ subseq (r \ s)" + unfolding subseq_def by simp (* TODO: move somewhere else *) + +lemma compact_union [intro]: + assumes "compact s" and "compact t" + shows "compact (s \ t)" +proof (rule compactI) + fix f :: "nat \ 'a" + assume "\n. f n \ s \ t" + hence "infinite {n. f n \ s \ t}" by simp + hence "infinite {n. f n \ s} \ infinite {n. f n \ t}" by simp + thus "\l\s \ t. \r. subseq r \ ((f \ r) ---> l) sequentially" + proof + assume "infinite {n. f n \ s}" + from infinite_enumerate [OF this] + obtain q where "subseq q" "\n. (f \ q) n \ s" by auto + obtain r l where "l \ s" "subseq r" "((f \ q \ r) ---> l) sequentially" + using `compact s` `\n. (f \ q) n \ s` by (rule compactE) + hence "l \ s \ t" "subseq (q \ r)" "((f \ (q \ r)) ---> l) sequentially" + using `subseq q` by (simp_all add: subseq_o o_assoc) + thus ?thesis by auto + next + assume "infinite {n. f n \ t}" + from infinite_enumerate [OF this] + obtain q where "subseq q" "\n. (f \ q) n \ t" by auto + obtain r l where "l \ t" "subseq r" "((f \ q \ r) ---> l) sequentially" + using `compact t` `\n. (f \ q) n \ t` by (rule compactE) + hence "l \ s \ t" "subseq (q \ r)" "((f \ (q \ r)) ---> l) sequentially" + using `subseq q` by (simp_all add: subseq_o o_assoc) + thus ?thesis by auto + qed +qed + +lemma compact_inter_closed [intro]: + assumes "compact s" and "closed t" + shows "compact (s \ t)" +proof (rule compactI) + fix f :: "nat \ 'a" + assume "\n. f n \ s \ t" + hence "\n. f n \ s" and "\n. f n \ t" by simp_all + obtain l r where "l \ s" "subseq r" "((f \ r) ---> l) sequentially" + using `compact s` `\n. f n \ s` by (rule compactE) moreover - have "s \ t = t \ s" by auto ultimately - show ?thesis - using compact_inter_closed[of t s] + from `closed t` `\n. f n \ t` `((f \ r) ---> l) sequentially` have "l \ t" + unfolding closed_sequential_limits o_def by fast + ultimately show "\l\s \ t. \r. subseq r \ ((f \ r) ---> l) sequentially" by auto qed -lemma finite_imp_compact: - fixes s :: "'a::heine_borel set" - shows "finite s ==> compact s" - unfolding compact_eq_bounded_closed - using finite_imp_closed finite_imp_bounded - by blast +lemma closed_inter_compact [intro]: + assumes "closed s" and "compact t" + shows "compact (s \ t)" + using compact_inter_closed [of t s] assms + by (simp add: Int_commute) + +lemma compact_inter [intro]: + assumes "compact s" and "compact t" + shows "compact (s \ t)" + using assms by (intro compact_inter_closed compact_imp_closed) lemma compact_sing [simp]: "compact {a}" unfolding compact_def o_def subseq_def by (auto simp add: tendsto_const) +lemma compact_insert [simp]: + assumes "compact s" shows "compact (insert x s)" +proof - + have "compact ({x} \ s)" + using compact_sing assms by (rule compact_union) + thus ?thesis by simp +qed + +lemma finite_imp_compact: + shows "finite s \ compact s" + by (induct set: finite) simp_all + lemma compact_cball[simp]: fixes x :: "'a::heine_borel" shows "compact(cball x e)" @@ -3102,7 +3139,6 @@ text{* Finite intersection property. I could make it an equivalence in fact. *} lemma compact_imp_fip: - fixes s :: "'a::heine_borel set" assumes "compact s" "\t \ f. closed t" "\f'. finite f' \ f' \ f --> (s \ (\ f') \ {})" shows "s \ (\ f) \ {}"