# HG changeset patch # User hoelzl # Date 1358182417 -3600 # Node ID 1421884baf5b871cc9914a7e147a3960bc1f8839 # Parent a382bf90867e4268064591487ce9f1289b96f866 introduce first_countable_topology typeclass diff -r a382bf90867e -r 1421884baf5b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 14 17:30:36 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 14 17:53:37 2013 +0100 @@ -239,6 +239,82 @@ end +class first_countable_topology = topological_space + + assumes first_countable_basis: + "\A. countable A \ (\a\A. x \ a \ open a) \ (\S. open S \ x \ S \ (\a\A. a \ S))" + +lemma (in first_countable_topology) countable_basis_at_decseq: + obtains A :: "nat \ 'a set" where + "\i. open (A i)" "\i. x \ (A i)" + "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially" +proof atomize_elim + from first_countable_basis[of x] obtain A + where "countable A" + and nhds: "\a. a \ A \ open a" "\a. a \ A \ x \ a" + and incl: "\S. open S \ x \ S \ \a\A. a \ S" by auto + then have "A \ {}" by auto + with `countable A` have r: "A = range (from_nat_into A)" by auto + def F \ "\n. \i\n. from_nat_into A i" + show "\A. (\i. open (A i)) \ (\i. x \ A i) \ + (\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially)" + proof (safe intro!: exI[of _ F]) + fix i + show "open (F i)" using nhds(1) r by (auto simp: F_def intro!: open_INT) + show "x \ F i" using nhds(2) r by (auto simp: F_def) + next + fix S assume "open S" "x \ S" + from incl[OF this] obtain i where "F i \ S" + by (subst (asm) r) (auto simp: F_def) + moreover have "\j. i \ j \ F j \ F i" + by (auto simp: F_def) + ultimately show "eventually (\i. F i \ S) sequentially" + by (auto simp: eventually_sequentially) + qed +qed + +lemma (in first_countable_topology) first_countable_basisE: + obtains A where "countable A" "\a. a \ A \ x \ a" "\a. a \ A \ open a" + "\S. open S \ x \ S \ (\a\A. a \ S)" + using first_countable_basis[of x] + by atomize_elim auto + +instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology +proof + fix x :: "'a \ 'b" + from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this + from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this + show "\A::('a\'b) set set. countable A \ (\a\A. x \ a \ open a) \ (\S. open S \ x \ S \ (\a\A. a \ S))" + proof (intro exI[of _ "(\(a, b). a \ b) ` (A \ B)"], safe) + fix a b assume x: "a \ A" "b \ B" + with A(2, 3)[of a] B(2, 3)[of b] show "x \ a \ b" "open (a \ b)" + unfolding mem_Times_iff by (auto intro: open_Times) + next + fix S assume "open S" "x \ S" + from open_prod_elim[OF this] guess a' b' . + moreover with A(4)[of a'] B(4)[of b'] + obtain a b where "a \ A" "a \ a'" "b \ B" "b \ b'" by auto + ultimately show "\a\(\(a, b). a \ b) ` (A \ B). a \ S" + by (auto intro!: bexI[of _ "a \ b"] bexI[of _ a] bexI[of _ b]) + qed (simp add: A B) +qed + +instance metric_space \ first_countable_topology +proof + fix x :: 'a + show "\A. countable A \ (\a\A. x \ a \ open a) \ (\S. open S \ x \ S \ (\a\A. a \ S))" + proof (intro exI, safe) + fix S assume "open S" "x \ S" + then obtain r where "0 < r" "{y. dist x y < r} \ S" + by (auto simp: open_dist dist_commute subset_eq) + moreover from reals_Archimedean[OF `0 < r`] guess n .. + moreover + then have "{y. dist x y < inverse (Suc n)} \ {y. dist x y < r}" + by (auto simp: inverse_eq_divide) + ultimately show "\a\range (\n. {y. dist x y < inverse (Suc n)}). a \ S" + by auto + qed (auto intro: open_ball) +qed + class second_countable_topology = topological_space + assumes ex_countable_basis: "\B::'a::topological_space set set. countable B \ topological_basis B" @@ -257,6 +333,18 @@ by (auto intro!: exI[of _ "(\(a, b). a \ b) ` (A \ B)"] topological_basis_prod) qed +instance second_countable_topology \ first_countable_topology +proof + fix x :: 'a + def B \ "SOME B::'a set set. countable B \ topological_basis B" + then have B: "countable B" "topological_basis B" + using countable_basis is_basis + by (auto simp: countable_basis is_basis) + then show "\A. countable A \ (\a\A. x \ a \ open a) \ (\S. open S \ x \ S \ (\a\A. a \ S))" + by (intro exI[of _ "{b\B. x \ b}"]) + (fastforce simp: topological_space_class.topological_basis_def) +qed + subsection {* Polish spaces *} text {* Textbooks define Polish spaces as completely metrizable. @@ -1350,33 +1438,38 @@ text{* Another limit point characterization. *} lemma islimpt_sequential: - fixes x :: "'a::metric_space" - shows "x islimpt S \ (\f. (\n::nat. f n \ S -{x}) \ (f ---> x) sequentially)" + fixes x :: "'a::first_countable_topology" + shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ (f ---> x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs - then obtain f where f:"\y. y>0 \ f y \ S \ f y \ x \ dist (f y) x < y" - unfolding islimpt_approachable - using choice[of "\e y. e>0 \ y\S \ y\x \ dist y x < e"] by auto - let ?I = "\n. inverse (real (Suc n))" - have "\n. f (?I n) \ S - {x}" using f by simp - moreover have "(\n. f (?I n)) ----> x" - proof (rule metric_tendsto_imp_tendsto) - show "?I ----> 0" - by (rule LIMSEQ_inverse_real_of_nat) - show "eventually (\n. dist (f (?I n)) x \ dist (?I n) 0) sequentially" - by (simp add: norm_conv_dist [symmetric] less_imp_le f) + from countable_basis_at_decseq[of x] guess A . note A = this + def f \ "\n. SOME y. y \ S \ y \ A n \ x \ y" + { fix n + from `?lhs` have "\y. y \ S \ y \ A n \ x \ y" + unfolding islimpt_def using A(1,2)[of n] by auto + then have "f n \ S \ f n \ A n \ x \ f n" + unfolding f_def by (rule someI_ex) + then have "f n \ S" "f n \ A n" "x \ f n" by auto } + then have "\n. f n \ S - {x}" by auto + moreover have "(\n. f n) ----> x" + proof (rule topological_tendstoI) + fix S assume "open S" "x \ S" + from A(3)[OF this] `\n. f n \ A n` + show "eventually (\x. f x \ S) sequentially" by (auto elim!: eventually_elim1) qed ultimately show ?rhs by fast next assume ?rhs - then obtain f::"nat\'a" where f:"(\n. f n \ S - {x})" "(\e>0. \N. \n\N. dist (f n) x < e)" unfolding LIMSEQ_def by auto - { fix e::real assume "e>0" - then obtain N where "dist (f N) x < e" using f(2) by auto - moreover have "f N\S" "f N \ x" using f(1) by auto - ultimately have "\x'\S. x' \ x \ dist x' x < e" by auto - } - thus ?lhs unfolding islimpt_approachable by auto + then obtain f :: "nat \ 'a" where f: "\n. f n \ S - {x}" and lim: "f ----> x" by auto + show ?lhs + unfolding islimpt_def + proof safe + fix T assume "open T" "x \ T" + from lim[THEN topological_tendstoD, OF this] f + show "\y\S. y \ T \ y \ x" + unfolding eventually_sequentially by auto + qed qed lemma Lim_inv: (* TODO: delete *) @@ -1626,7 +1719,7 @@ text{* Useful lemmas on closure and set of possible sequential limits.*} lemma closure_sequential: - fixes l :: "'a::metric_space" + fixes l :: "'a::first_countable_topology" shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" (is "?lhs = ?rhs") proof assume "?lhs" moreover @@ -1643,7 +1736,7 @@ qed lemma closed_sequential_limits: - fixes S :: "'a::metric_space set" + 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] @@ -2778,74 +2871,37 @@ subsubsection {* Complete the chain of compactness variants *} lemma islimpt_range_imp_convergent_subsequence: - fixes f :: "nat \ 'a::metric_space" - assumes "l islimpt (range f)" + fixes l :: "'a :: {t1_space, first_countable_topology}" + assumes l: "l islimpt (range f)" shows "\r. subseq r \ ((f \ r) ---> l) sequentially" -proof (intro exI conjI) - have *: "\e. 0 < e \ \n. 0 < dist (f n) l \ dist (f n) l < e" - using assms unfolding islimpt_def - by (drule_tac x="ball l e" in spec) - (auto simp add: zero_less_dist_iff dist_commute) - - def t \ "\e. LEAST n. 0 < dist (f n) l \ dist (f n) l < e" - have f_t_neq: "\e. 0 < e \ 0 < dist (f (t e)) l" - unfolding t_def by (rule LeastI2_ex [OF * conjunct1]) - have f_t_closer: "\e. 0 < e \ dist (f (t e)) l < e" - unfolding t_def by (rule LeastI2_ex [OF * conjunct2]) - have t_le: "\n e. 0 < dist (f n) l \ dist (f n) l < e \ t e \ n" - unfolding t_def by (simp add: Least_le) - have less_tD: "\n e. n < t e \ 0 < dist (f n) l \ e \ dist (f n) l" - unfolding t_def by (drule not_less_Least) simp - have t_antimono: "\e e'. 0 < e \ e \ e' \ t e' \ t e" - apply (rule t_le) - apply (erule f_t_neq) - apply (erule (1) less_le_trans [OF f_t_closer]) - done - have t_dist_f_neq: "\n. 0 < dist (f n) l \ t (dist (f n) l) \ n" - by (drule f_t_closer) auto - have t_less: "\e. 0 < e \ t e < t (dist (f (t e)) l)" - apply (subst less_le) - apply (rule conjI) - apply (rule t_antimono) - apply (erule f_t_neq) - apply (erule f_t_closer [THEN less_imp_le]) - apply (rule t_dist_f_neq [symmetric]) - apply (erule f_t_neq) - done - have dist_f_t_less': - "\e e'. 0 < e \ 0 < e' \ t e \ t e' \ dist (f (t e')) l < e" - apply (simp add: le_less) - apply (erule disjE) - apply (rule less_trans) - apply (erule f_t_closer) - apply (rule le_less_trans) - apply (erule less_tD) - apply (erule f_t_neq) - apply (erule f_t_closer) - apply (erule subst) - apply (erule f_t_closer) - done - - def r \ "nat_rec (t 1) (\_ x. t (dist (f x) l))" - have r_simps: "r 0 = t 1" "\n. r (Suc n) = t (dist (f (r n)) l)" - unfolding r_def by simp_all - have f_r_neq: "\n. 0 < dist (f (r n)) l" - by (induct_tac n) (simp_all add: r_simps f_t_neq) - - show "subseq r" - unfolding subseq_Suc_iff - apply (rule allI) - apply (case_tac n) - apply (simp_all add: r_simps) - apply (rule t_less, rule zero_less_one) - apply (rule t_less, rule f_r_neq) - done - show "((f \ r) ---> l) sequentially" - unfolding LIMSEQ_def o_def - apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify) - apply (drule le_trans, rule seq_suble [OF `subseq r`]) - apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq) - done +proof - + from first_countable_topology_class.countable_basis_at_decseq[of l] guess A . note A = this + + def s \ "\n i. SOME j. i < j \ f j \ A (Suc n)" + { fix n i + have "\a. i < a \ f a \ A (Suc n)" + by (rule l[THEN islimptE, of "A (Suc n) - (f ` {.. i} - {l})"]) + (auto simp: not_le[symmetric] finite_imp_closed A(1,2)) + then have "i < s n i" "f (s n i) \ A (Suc n)" + unfolding s_def by (auto intro: someI2_ex) } + note s = this + def r \ "nat_rec (s 0 0) s" + have "subseq r" + by (auto simp: r_def s subseq_Suc_iff) + moreover + have "(\n. f (r n)) ----> l" + proof (rule topological_tendstoI) + fix S assume "open S" "l \ S" + with A(3) have "eventually (\i. A i \ S) sequentially" by auto + moreover + { fix i assume "Suc 0 \ i" then have "f (r i) \ A i" + by (cases i) (simp_all add: r_def s) } + then have "eventually (\i. f (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) + ultimately show "eventually (\i. f (r i) \ S) sequentially" + by eventually_elim auto + qed + ultimately show "\r. subseq r \ (f \ r) ----> l" + by (auto simp: convergent_def comp_def) qed lemma finite_range_imp_infinite_repeats: