author hoelzl Mon Jan 14 17:53:37 2013 +0100 (2013-01-14) changeset 50883 1421884baf5b parent 50882 a382bf90867e child 50884 2b21b4e2d7cb
introduce first_countable_topology typeclass
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:30:36 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:53:37 2013 +0100
1.3 @@ -239,6 +239,82 @@
1.4
1.5  end
1.6
1.7 +class first_countable_topology = topological_space +
1.8 +  assumes first_countable_basis:
1.9 +    "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
1.10 +
1.11 +lemma (in first_countable_topology) countable_basis_at_decseq:
1.12 +  obtains A :: "nat \<Rightarrow> 'a set" where
1.13 +    "\<And>i. open (A i)" "\<And>i. x \<in> (A i)"
1.14 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
1.15 +proof atomize_elim
1.16 +  from first_countable_basis[of x] obtain A
1.17 +    where "countable A"
1.18 +    and nhds: "\<And>a. a \<in> A \<Longrightarrow> open a" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a"
1.19 +    and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"  by auto
1.20 +  then have "A \<noteq> {}" by auto
1.21 +  with `countable A` have r: "A = range (from_nat_into A)" by auto
1.22 +  def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. from_nat_into A i"
1.23 +  show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and>
1.24 +      (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
1.25 +  proof (safe intro!: exI[of _ F])
1.26 +    fix i
1.27 +    show "open (F i)" using nhds(1) r by (auto simp: F_def intro!: open_INT)
1.28 +    show "x \<in> F i" using nhds(2) r by (auto simp: F_def)
1.29 +  next
1.30 +    fix S assume "open S" "x \<in> S"
1.31 +    from incl[OF this] obtain i where "F i \<subseteq> S"
1.32 +      by (subst (asm) r) (auto simp: F_def)
1.33 +    moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
1.34 +      by (auto simp: F_def)
1.35 +    ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
1.36 +      by (auto simp: eventually_sequentially)
1.37 +  qed
1.38 +qed
1.39 +
1.40 +lemma (in first_countable_topology) first_countable_basisE:
1.41 +  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
1.42 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
1.43 +  using first_countable_basis[of x]
1.44 +  by atomize_elim auto
1.45 +
1.46 +instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
1.47 +proof
1.48 +  fix x :: "'a \<times> 'b"
1.49 +  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
1.50 +  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
1.51 +  show "\<exists>A::('a\<times>'b) set set. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
1.52 +  proof (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
1.53 +    fix a b assume x: "a \<in> A" "b \<in> B"
1.54 +    with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
1.55 +      unfolding mem_Times_iff by (auto intro: open_Times)
1.56 +  next
1.57 +    fix S assume "open S" "x \<in> S"
1.58 +    from open_prod_elim[OF this] guess a' b' .
1.59 +    moreover with A(4)[of a'] B(4)[of b']
1.60 +    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
1.61 +    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
1.62 +      by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
1.63 +  qed (simp add: A B)
1.64 +qed
1.65 +
1.66 +instance metric_space \<subseteq> first_countable_topology
1.67 +proof
1.68 +  fix x :: 'a
1.69 +  show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
1.70 +  proof (intro exI, safe)
1.71 +    fix S assume "open S" "x \<in> S"
1.72 +    then obtain r where "0 < r" "{y. dist x y < r} \<subseteq> S"
1.73 +      by (auto simp: open_dist dist_commute subset_eq)
1.74 +    moreover from reals_Archimedean[OF `0 < r`] guess n ..
1.75 +    moreover
1.76 +    then have "{y. dist x y < inverse (Suc n)} \<subseteq> {y. dist x y < r}"
1.77 +      by (auto simp: inverse_eq_divide)
1.78 +    ultimately show "\<exists>a\<in>range (\<lambda>n. {y. dist x y < inverse (Suc n)}). a \<subseteq> S"
1.79 +      by auto
1.80 +  qed (auto intro: open_ball)
1.81 +qed
1.82 +
1.83  class second_countable_topology = topological_space +
1.84    assumes ex_countable_basis:
1.85      "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
1.86 @@ -257,6 +333,18 @@
1.87      by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
1.88  qed
1.89
1.90 +instance second_countable_topology \<subseteq> first_countable_topology
1.91 +proof
1.92 +  fix x :: 'a
1.93 +  def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B"
1.94 +  then have B: "countable B" "topological_basis B"
1.95 +    using countable_basis is_basis
1.96 +    by (auto simp: countable_basis is_basis)
1.97 +  then show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
1.98 +    by (intro exI[of _ "{b\<in>B. x \<in> b}"])
1.99 +       (fastforce simp: topological_space_class.topological_basis_def)
1.100 +qed
1.101 +
1.102  subsection {* Polish spaces *}
1.103
1.104  text {* Textbooks define Polish spaces as completely metrizable.
1.105 @@ -1350,33 +1438,38 @@
1.106  text{* Another limit point characterization. *}
1.107
1.108  lemma islimpt_sequential:
1.109 -  fixes x :: "'a::metric_space"
1.110 -  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
1.111 +  fixes x :: "'a::first_countable_topology"
1.112 +  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f ---> x) sequentially)"
1.113      (is "?lhs = ?rhs")
1.114  proof
1.115    assume ?lhs
1.116 -  then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
1.117 -    unfolding islimpt_approachable
1.118 -    using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
1.119 -  let ?I = "\<lambda>n. inverse (real (Suc n))"
1.120 -  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
1.121 -  moreover have "(\<lambda>n. f (?I n)) ----> x"
1.122 -  proof (rule metric_tendsto_imp_tendsto)
1.123 -    show "?I ----> 0"
1.124 -      by (rule LIMSEQ_inverse_real_of_nat)
1.125 -    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
1.126 -      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
1.127 +  from countable_basis_at_decseq[of x] guess A . note A = this
1.128 +  def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
1.129 +  { fix n
1.130 +    from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
1.131 +      unfolding islimpt_def using A(1,2)[of n] by auto
1.132 +    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
1.133 +      unfolding f_def by (rule someI_ex)
1.134 +    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
1.135 +  then have "\<forall>n. f n \<in> S - {x}" by auto
1.136 +  moreover have "(\<lambda>n. f n) ----> x"
1.137 +  proof (rule topological_tendstoI)
1.138 +    fix S assume "open S" "x \<in> S"
1.139 +    from A(3)[OF this] `\<And>n. f n \<in> A n`
1.140 +    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
1.141    qed
1.142    ultimately show ?rhs by fast
1.143  next
1.144    assume ?rhs
1.145 -  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding LIMSEQ_def by auto
1.146 -  { fix e::real assume "e>0"
1.147 -    then obtain N where "dist (f N) x < e" using f(2) by auto
1.148 -    moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
1.149 -    ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto
1.150 -  }
1.151 -  thus ?lhs unfolding islimpt_approachable by auto
1.152 +  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
1.153 +  show ?lhs
1.154 +    unfolding islimpt_def
1.155 +  proof safe
1.156 +    fix T assume "open T" "x \<in> T"
1.157 +    from lim[THEN topological_tendstoD, OF this] f
1.158 +    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
1.159 +      unfolding eventually_sequentially by auto
1.160 +  qed
1.161  qed
1.162
1.163  lemma Lim_inv: (* TODO: delete *)
1.164 @@ -1626,7 +1719,7 @@
1.165  text{* Useful lemmas on closure and set of possible sequential limits.*}
1.166
1.167  lemma closure_sequential:
1.168 -  fixes l :: "'a::metric_space"
1.169 +  fixes l :: "'a::first_countable_topology"
1.170    shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
1.171  proof
1.172    assume "?lhs" moreover
1.173 @@ -1643,7 +1736,7 @@
1.174  qed
1.175
1.176  lemma closed_sequential_limits:
1.177 -  fixes S :: "'a::metric_space set"
1.178 +  fixes S :: "'a::first_countable_topology set"
1.179    shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
1.180    unfolding closed_limpt
1.181    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]
1.182 @@ -2778,74 +2871,37 @@
1.183  subsubsection {* Complete the chain of compactness variants *}
1.184
1.185  lemma islimpt_range_imp_convergent_subsequence:
1.186 -  fixes f :: "nat \<Rightarrow> 'a::metric_space"
1.187 -  assumes "l islimpt (range f)"
1.188 +  fixes l :: "'a :: {t1_space, first_countable_topology}"
1.189 +  assumes l: "l islimpt (range f)"
1.190    shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
1.191 -proof (intro exI conjI)
1.192 -  have *: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. 0 < dist (f n) l \<and> dist (f n) l < e"
1.193 -    using assms unfolding islimpt_def
1.194 -    by (drule_tac x="ball l e" in spec)
1.195 -       (auto simp add: zero_less_dist_iff dist_commute)
1.196 -
1.197 -  def t \<equiv> "\<lambda>e. LEAST n. 0 < dist (f n) l \<and> dist (f n) l < e"
1.198 -  have f_t_neq: "\<And>e. 0 < e \<Longrightarrow> 0 < dist (f (t e)) l"
1.199 -    unfolding t_def by (rule LeastI2_ex [OF * conjunct1])
1.200 -  have f_t_closer: "\<And>e. 0 < e \<Longrightarrow> dist (f (t e)) l < e"
1.201 -    unfolding t_def by (rule LeastI2_ex [OF * conjunct2])
1.202 -  have t_le: "\<And>n e. 0 < dist (f n) l \<Longrightarrow> dist (f n) l < e \<Longrightarrow> t e \<le> n"
1.203 -    unfolding t_def by (simp add: Least_le)
1.204 -  have less_tD: "\<And>n e. n < t e \<Longrightarrow> 0 < dist (f n) l \<Longrightarrow> e \<le> dist (f n) l"
1.205 -    unfolding t_def by (drule not_less_Least) simp
1.206 -  have t_antimono: "\<And>e e'. 0 < e \<Longrightarrow> e \<le> e' \<Longrightarrow> t e' \<le> t e"
1.207 -    apply (rule t_le)
1.208 -    apply (erule f_t_neq)
1.209 -    apply (erule (1) less_le_trans [OF f_t_closer])
1.210 -    done
1.211 -  have t_dist_f_neq: "\<And>n. 0 < dist (f n) l \<Longrightarrow> t (dist (f n) l) \<noteq> n"
1.212 -    by (drule f_t_closer) auto
1.213 -  have t_less: "\<And>e. 0 < e \<Longrightarrow> t e < t (dist (f (t e)) l)"
1.214 -    apply (subst less_le)
1.215 -    apply (rule conjI)
1.216 -    apply (rule t_antimono)
1.217 -    apply (erule f_t_neq)
1.218 -    apply (erule f_t_closer [THEN less_imp_le])
1.219 -    apply (rule t_dist_f_neq [symmetric])
1.220 -    apply (erule f_t_neq)
1.221 -    done
1.222 -  have dist_f_t_less':
1.223 -    "\<And>e e'. 0 < e \<Longrightarrow> 0 < e' \<Longrightarrow> t e \<le> t e' \<Longrightarrow> dist (f (t e')) l < e"
1.224 -    apply (simp add: le_less)
1.225 -    apply (erule disjE)
1.226 -    apply (rule less_trans)
1.227 -    apply (erule f_t_closer)
1.228 -    apply (rule le_less_trans)
1.229 -    apply (erule less_tD)
1.230 -    apply (erule f_t_neq)
1.231 -    apply (erule f_t_closer)
1.232 -    apply (erule subst)
1.233 -    apply (erule f_t_closer)
1.234 -    done
1.235 -
1.236 -  def r \<equiv> "nat_rec (t 1) (\<lambda>_ x. t (dist (f x) l))"
1.237 -  have r_simps: "r 0 = t 1" "\<And>n. r (Suc n) = t (dist (f (r n)) l)"
1.238 -    unfolding r_def by simp_all
1.239 -  have f_r_neq: "\<And>n. 0 < dist (f (r n)) l"
1.240 -    by (induct_tac n) (simp_all add: r_simps f_t_neq)
1.241 -
1.242 -  show "subseq r"
1.243 -    unfolding subseq_Suc_iff
1.244 -    apply (rule allI)
1.245 -    apply (case_tac n)
1.246 -    apply (simp_all add: r_simps)
1.247 -    apply (rule t_less, rule zero_less_one)
1.248 -    apply (rule t_less, rule f_r_neq)
1.249 -    done
1.250 -  show "((f \<circ> r) ---> l) sequentially"
1.251 -    unfolding LIMSEQ_def o_def
1.252 -    apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify)
1.253 -    apply (drule le_trans, rule seq_suble [OF `subseq r`])
1.254 -    apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq)
1.255 -    done
1.256 +proof -
1.257 +  from first_countable_topology_class.countable_basis_at_decseq[of l] guess A . note A = this
1.258 +
1.259 +  def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
1.260 +  { fix n i
1.261 +    have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
1.262 +      by (rule l[THEN islimptE, of "A (Suc n) - (f ` {.. i} - {l})"])
1.263 +         (auto simp: not_le[symmetric] finite_imp_closed A(1,2))
1.264 +    then have "i < s n i" "f (s n i) \<in> A (Suc n)"
1.265 +      unfolding s_def by (auto intro: someI2_ex) }
1.266 +  note s = this
1.267 +  def r \<equiv> "nat_rec (s 0 0) s"
1.268 +  have "subseq r"
1.269 +    by (auto simp: r_def s subseq_Suc_iff)
1.270 +  moreover
1.271 +  have "(\<lambda>n. f (r n)) ----> l"
1.272 +  proof (rule topological_tendstoI)
1.273 +    fix S assume "open S" "l \<in> S"
1.274 +    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
1.275 +    moreover
1.276 +    { fix i assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
1.277 +        by (cases i) (simp_all add: r_def s) }
1.278 +    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
1.279 +    ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
1.280 +      by eventually_elim auto
1.281 +  qed
1.282 +  ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
1.283 +    by (auto simp: convergent_def comp_def)
1.284  qed
1.285
1.286  lemma finite_range_imp_infinite_repeats:
```