# HG changeset patch # User huffman # Date 1358267396 28800 # Node ID ebd9b82537e08f9babe581120e60f11202eadaa9 # Parent 0785906695276381efa35d514e05d4011d7dc525 generalized more topology theorems diff -r 078590669527 -r ebd9b82537e0 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 14 19:28:39 2013 -0800 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jan 15 08:29:56 2013 -0800 @@ -2339,6 +2339,16 @@ compact_eq_heine_borel: -- "This name is used for backwards compatibility" "compact S \ (\C. (\c\C. open c) \ S \ \C \ (\D\C. finite D \ S \ \D))" +lemma compactI: + assumes "\C. \t\C. open t \ s \ \ C \ \C'. C' \ C \ finite C' \ s \ \ C'" + shows "compact s" + unfolding compact_eq_heine_borel using assms by metis + +lemma compactE: + assumes "compact s" and "\t\C. open t" and "s \ \C" + obtains C' where "C' \ C" and "finite C'" and "s \ \C'" + using assms unfolding compact_eq_heine_borel by metis + subsubsection {* Bolzano-Weierstrass property *} lemma heine_borel_imp_bolzano_weierstrass: @@ -2537,14 +2547,32 @@ qed lemma compact_imp_closed: - fixes s :: "'a::{first_countable_topology, t2_space} set" - shows "compact s \ closed s" -proof - - assume "compact s" - hence "\t. infinite t \ t \ s \ (\x \ s. x islimpt t)" - using heine_borel_imp_bolzano_weierstrass[of s] by auto - thus "closed s" - by (rule bolzano_weierstrass_imp_closed) + fixes s :: "'a::t2_space set" + assumes "compact s" shows "closed s" +unfolding closed_def +proof (rule openI) + fix y assume "y \ - s" + let ?C = "\x\s. {u. open u \ x \ u \ eventually (\y. y \ u) (nhds y)}" + note `compact s` + moreover have "\u\?C. open u" by simp + moreover have "s \ \?C" + proof + fix x assume "x \ s" + with `y \ - s` have "x \ y" by clarsimp + hence "\u v. open u \ open v \ x \ u \ y \ v \ u \ v = {}" + by (rule hausdorff) + with `x \ s` show "x \ \?C" + unfolding eventually_nhds by auto + qed + ultimately obtain D where "D \ ?C" and "finite D" and "s \ \D" + by (rule compactE) + from `D \ ?C` have "\x\D. eventually (\y. y \ x) (nhds y)" by auto + with `finite D` have "eventually (\y. y \ \D) (nhds y)" + by (simp add: eventually_Ball_finite) + with `s \ \D` have "eventually (\y. y \ s) (nhds y)" + by (auto elim!: eventually_mono [rotated]) + thus "\t. open t \ y \ t \ t \ - s" + by (simp add: eventually_nhds subset_eq) qed text{* In particular, some common special cases. *} @@ -2556,9 +2584,8 @@ lemma compact_union [intro]: assumes "compact s" "compact t" shows " compact (s \ t)" - unfolding compact_eq_heine_borel -proof (intro allI impI) - fix f assume *: "Ball f open \ s \ t \ \f" +proof (rule compactI) + fix f assume *: "Ball f open" "s \ t \ \f" from * `compact s` obtain s' where "s' \ f \ finite s' \ s \ \s'" unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis moreover from * `compact t` obtain t' where "t' \ f \ finite t' \ t \ \t'" @@ -2577,8 +2604,7 @@ lemma compact_inter_closed [intro]: assumes "compact s" and "closed t" shows "compact (s \ t)" - unfolding compact_eq_heine_borel -proof safe +proof (rule compactI) fix C assume C: "\c\C. open c" and cover: "s \ t \ \C" from C `closed t` have "\c\C \ {-t}. open c" by auto moreover from cover have "s \ \(C \ {-t})" by auto @@ -2596,7 +2622,7 @@ by (simp add: Int_commute) lemma compact_inter [intro]: - fixes s t :: "'a :: {t2_space, first_countable_topology} set" + fixes s t :: "'a :: t2_space set" assumes "compact s" and "compact t" shows "compact (s \ t)" using assms by (intro compact_inter_closed compact_imp_closed) @@ -4621,35 +4647,41 @@ text {* Making a continuous function avoid some value in a neighbourhood. *} lemma continuous_within_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) - assumes "continuous (at x within s) f" "x \ s" "f x \ a" + fixes f :: "'a::metric_space \ 'b::t1_space" + assumes "continuous (at x within s) f" and "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" proof- - obtain d where "d>0" and d:"\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < dist (f x) a" - using assms(1)[unfolded continuous_within Lim_within, THEN spec[where x="dist (f x) a"]] assms(3)[unfolded dist_nz] by auto - { fix y assume " y\s" "dist x y < d" - hence "f y \ a" using d[THEN bspec[where x=y]] assms(3)[unfolded dist_nz] - apply auto unfolding dist_nz[THEN sym] by (auto simp add: dist_commute) } - thus ?thesis using `d>0` by auto + obtain U where "open U" and "f x \ U" and "a \ U" + using t1_space [OF `f x \ a`] by fast + have "(f ---> f x) (at x within s)" + using assms(1) by (simp add: continuous_within) + hence "eventually (\y. f y \ U) (at x within s)" + using `open U` and `f x \ U` + unfolding tendsto_def by fast + hence "eventually (\y. f y \ a) (at x within s)" + using `a \ U` by (fast elim: eventually_mono [rotated]) + thus ?thesis + unfolding Limits.eventually_within Limits.eventually_at + by (rule ex_forward, cut_tac `f x \ a`, auto simp: dist_commute) qed lemma continuous_at_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x) f" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms continuous_within_avoid[of x UNIV f a] by simp lemma continuous_on_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* TODO: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" "x \ s" "f x \ a" shows "\e>0. \y \ s. dist x y < e \ f y \ a" -using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] assms(2,3) by auto +using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] assms(3) by auto lemma continuous_on_open_avoid: - fixes f :: "'a::metric_space \ 'b::metric_space" (* TODO: generalize *) + fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" "open s" "x \ s" "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" -using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(3,4) by auto +using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(4) by auto text {* Proving a function is constant by proving open-ness of level set. *} @@ -4790,23 +4822,83 @@ text {* Preservation of compactness and connectedness under continuous function. *} +lemma compact_eq_openin_cover: + "compact S \ + (\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \ + (\D\C. finite D \ S \ \D))" +proof safe + fix C + assume "compact S" and "\c\C. openin (subtopology euclidean S) c" and "S \ \C" + hence "\c\{T. open T \ S \ T \ C}. open c" and "S \ \{T. open T \ S \ T \ C}" + unfolding openin_open by force+ + with `compact S` obtain D where "D \ {T. open T \ S \ T \ C}" and "finite D" and "S \ \D" + by (rule compactE) + hence "image (\T. S \ T) D \ C \ finite (image (\T. S \ T) D) \ S \ \(image (\T. S \ T) D)" + by auto + thus "\D\C. finite D \ S \ \D" .. +next + assume 1: "\C. (\c\C. openin (subtopology euclidean S) c) \ S \ \C \ + (\D\C. finite D \ S \ \D)" + show "compact S" + proof (rule compactI) + fix C + let ?C = "image (\T. S \ T) C" + assume "\t\C. open t" and "S \ \C" + hence "(\c\?C. openin (subtopology euclidean S) c) \ S \ \?C" + unfolding openin_open by auto + with 1 obtain D where "D \ ?C" and "finite D" and "S \ \D" + by metis + let ?D = "inv_into C (\T. S \ T) ` D" + have "?D \ C \ finite ?D \ S \ \?D" + proof (intro conjI) + from `D \ ?C` show "?D \ C" + by (fast intro: inv_into_into) + from `finite D` show "finite ?D" + by (rule finite_imageI) + from `S \ \D` show "S \ \?D" + apply (rule subset_trans) + apply clarsimp + apply (frule subsetD [OF `D \ ?C`, THEN f_inv_into_f]) + apply (erule rev_bexI, fast) + done + qed + thus "\D\C. finite D \ S \ \D" .. + qed +qed + lemma compact_continuous_image: - fixes f :: "'a :: metric_space \ 'b :: metric_space" - assumes "continuous_on s f" "compact s" - shows "compact(f ` s)" -proof- - { fix x assume x:"\n::nat. x n \ f ` s" - then obtain y where y:"\n. y n \ s \ x n = f (y n)" unfolding image_iff Bex_def using choice[of "\n xa. xa \ s \ x n = f xa"] by auto - then obtain l r where "l\s" and r:"subseq r" and lr:"((y \ r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto - { fix e::real assume "e>0" - then obtain d where "d>0" and d:"\x'\s. dist x' l < d \ dist (f x') (f l) < e" - using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\s`] by auto - then obtain N::nat where N:"\n\N. dist ((y \ r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto - { fix n::nat assume "n\N" hence "dist ((x \ r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto } - hence "\N. \n\N. dist ((x \ r) n) (f l) < e" by auto } - hence "\l\f ` s. \r. subseq r \ ((x \ r) ---> l) sequentially" unfolding LIMSEQ_def using r lr `l\s` by auto } - thus ?thesis unfolding compact_def by auto -qed + assumes "continuous_on s f" and "compact s" + shows "compact (f ` s)" +using assms (* FIXME: long unstructured proof *) +unfolding continuous_on_open +unfolding compact_eq_openin_cover +apply clarify +apply (drule_tac x="image (\t. {x \ s. f x \ t}) C" in spec) +apply (drule mp) +apply (rule conjI) +apply simp +apply clarsimp +apply (drule subsetD) +apply (erule imageI) +apply fast +apply (erule thin_rl) +apply clarify +apply (rule_tac x="image (inv_into C (\t. {x \ s. f x \ t})) D" in exI) +apply (intro conjI) +apply clarify +apply (rule inv_into_into) +apply (erule (1) subsetD) +apply (erule finite_imageI) +apply (clarsimp, rename_tac x) +apply (drule (1) subsetD, clarify) +apply (drule (1) subsetD, clarify) +apply (rule rev_bexI) +apply assumption +apply (subgoal_tac "{x \ s. f x \ t} \ (\t. {x \ s. f x \ t}) ` C") +apply (drule f_inv_into_f) +apply fast +apply (erule imageI) +done lemma connected_continuous_image: assumes "continuous_on s f" "connected s" @@ -4862,25 +4954,33 @@ text{* Continuity of inverse function on compact domain. *} lemma continuous_on_inv: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* TODO: can this be generalized more? *) + fixes f :: "'a::topological_space \ 'b::t2_space" assumes "continuous_on s f" "compact s" "\x \ s. g (f x) = x" shows "continuous_on (f ` s) g" -proof- - have *:"g ` f ` s = s" using assms(3) by (auto simp add: image_iff) - { fix t assume t:"closedin (subtopology euclidean (g ` f ` s)) t" - then obtain T where T: "closed T" "t = s \ T" unfolding closedin_closed unfolding * by auto - have "continuous_on (s \ T) f" using continuous_on_subset[OF assms(1), of "s \ t"] - unfolding T(2) and Int_left_absorb by auto - moreover have "compact (s \ T)" - using assms(2) unfolding compact_eq_bounded_closed - using bounded_subset[of s "s \ T"] and T(1) by auto - ultimately have "closed (f ` t)" using T(1) unfolding T(2) - using compact_continuous_image [of "s \ T" f] unfolding compact_eq_bounded_closed by auto - moreover have "{x \ f ` s. g x \ t} = f ` s \ f ` t" using assms(3) unfolding T(2) by auto - ultimately have "closedin (subtopology euclidean (f ` s)) {x \ f ` s. g x \ t}" - unfolding closedin_closed by auto } - thus ?thesis unfolding continuous_on_closed by auto +unfolding continuous_on_topological +proof (clarsimp simp add: assms(3)) + fix x :: 'a and B :: "'a set" + assume "x \ s" and "open B" and "x \ B" + have 1: "\x\s. f x \ f ` (s - B) \ x \ s - B" + using assms(3) by (auto, metis) + have "continuous_on (s - B) f" + using `continuous_on s f` Diff_subset + by (rule continuous_on_subset) + moreover have "compact (s - B)" + using `open B` and `compact s` + unfolding Diff_eq by (intro compact_inter_closed closed_Compl) + ultimately have "compact (f ` (s - B))" + by (rule compact_continuous_image) + hence "closed (f ` (s - B))" + by (rule compact_imp_closed) + hence "open (- f ` (s - B))" + by (rule open_Compl) + moreover have "f x \ - f ` (s - B)" + using `x \ s` and `x \ B` by (simp add: 1) + moreover have "\y\s. f y \ - f ` (s - B) \ y \ B" + by (simp add: 1) + ultimately show "\A. open A \ f x \ A \ (\y\s. f y \ A \ y \ B)" + by fast qed text {* A uniformly convergent limit of continuous functions is continuous. *} @@ -6043,7 +6143,7 @@ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" definition - homeomorphic :: "'a::metric_space set \ 'b::metric_space set \ bool" + homeomorphic :: "'a::topological_space set \ 'b::topological_space set \ bool" (infixr "homeomorphic" 60) where homeomorphic_def: "s homeomorphic t \ (\f g. homeomorphism s t f g)" @@ -6095,8 +6195,7 @@ text {* Relatively weak hypotheses if a set is compact. *} lemma homeomorphism_compact: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* class constraint due to continuous_on_inv *) + fixes f :: "'a::topological_space \ 'b::t2_space" assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof- @@ -6123,8 +6222,7 @@ qed lemma homeomorphic_compact: - fixes f :: "'a::heine_borel \ 'b::heine_borel" - (* class constraint due to continuous_on_inv *) + fixes f :: "'a::topological_space \ 'b::t2_space" shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by (metis homeomorphism_compact) @@ -6166,12 +6264,11 @@ qed lemma homeomorphic_balls: - fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *) + fixes a b ::"'a::real_normed_vector" assumes "0 < d" "0 < e" shows "(ball a d) homeomorphic (ball b e)" (is ?th) "(cball a d) homeomorphic (cball b e)" (is ?cth) proof- - have *:"\e / d\ > 0" "\d / e\ >0" using assms using divide_pos_pos by auto show ?th unfolding homeomorphic_minimal apply(rule_tac x="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\x. a + (d/e) *\<^sub>R (x - b)" in exI) @@ -6181,7 +6278,6 @@ unfolding continuous_on by (intro ballI tendsto_intros, simp)+ next - have *:"\e / d\ > 0" "\d / e\ >0" using assms using divide_pos_pos by auto show ?cth unfolding homeomorphic_minimal apply(rule_tac x="\x. b + (e/d) *\<^sub>R (x - a)" in exI) apply(rule_tac x="\x. a + (d/e) *\<^sub>R (x - b)" in exI)