src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50245 dea9363887a6
parent 50105 65d5b18e1626
child 50324 0a1242d5e7d4
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  imports
     1.5    SEQ
     1.6    "~~/src/HOL/Library/Diagonal_Subsequence"
     1.7 -  "~~/src/HOL/Library/Countable"
     1.8 +  "~~/src/HOL/Library/Countable_Set"
     1.9    Linear_Algebra
    1.10    "~~/src/HOL/Library/Glbs"
    1.11    Norm_Arith
    1.12 @@ -71,147 +71,160 @@
    1.13    using assms
    1.14    by (simp add: topological_basis_def)
    1.15  
    1.16 +lemma basis_dense:
    1.17 +  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
    1.18 +  assumes "topological_basis B"
    1.19 +  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
    1.20 +  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
    1.21 +proof (intro allI impI)
    1.22 +  fix X::"'a set" assume "open X" "X \<noteq> {}"
    1.23 +  from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
    1.24 +  guess B' . note B' = this
    1.25 +  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
    1.26 +qed
    1.27 +
    1.28  end
    1.29  
    1.30 -subsection {* Enumerable Basis *}
    1.31 -
    1.32 -locale enumerates_basis =
    1.33 -  fixes f::"nat \<Rightarrow> 'a::topological_space set"
    1.34 -  assumes enumerable_basis: "topological_basis (range f)"
    1.35 +subsection {* Countable Basis *}
    1.36 +
    1.37 +locale countable_basis =
    1.38 +  fixes B::"'a::topological_space set set"
    1.39 +  assumes is_basis: "topological_basis B"
    1.40 +  assumes countable_basis: "countable B"
    1.41  begin
    1.42  
    1.43 -lemma open_enumerable_basis_ex:
    1.44 -  assumes "open X"
    1.45 -  shows "\<exists>N. X = (\<Union>n\<in>N. f n)"
    1.46 -proof -
    1.47 -  from enumerable_basis assms obtain B' where "B' \<subseteq> range f" "X = Union B'"
    1.48 -    unfolding topological_basis_def by blast
    1.49 -  hence "Union B' = (\<Union>n\<in>{n. f n \<in> B'}. f n)" by auto
    1.50 -  with `X = Union B'` show ?thesis by blast
    1.51 -qed
    1.52 -
    1.53 -lemma open_enumerable_basisE:
    1.54 +lemma open_countable_basis_ex:
    1.55    assumes "open X"
    1.56 -  obtains N where "X = (\<Union>n\<in>N. f n)"
    1.57 -  using assms open_enumerable_basis_ex by (atomize_elim) simp
    1.58 -
    1.59 -lemma countable_dense_set:
    1.60 -  shows "\<exists>x::nat \<Rightarrow> 'a. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
    1.61 +  shows "\<exists>B' \<subseteq> B. X = Union B'"
    1.62 +  using assms countable_basis is_basis unfolding topological_basis_def by blast
    1.63 +
    1.64 +lemma open_countable_basisE:
    1.65 +  assumes "open X"
    1.66 +  obtains B' where "B' \<subseteq> B" "X = Union B'"
    1.67 +  using assms open_countable_basis_ex by (atomize_elim) simp
    1.68 +
    1.69 +lemma countable_dense_exists:
    1.70 +  shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
    1.71  proof -
    1.72 -  def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> f n)"
    1.73 -  have x: "\<And>n. f n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> f n" unfolding x_def
    1.74 -    by (rule someI_ex) auto
    1.75 -  have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
    1.76 -  proof (intro allI impI)
    1.77 -    fix y::"'a set" assume "open y" "y \<noteq> {}"
    1.78 -    from open_enumerable_basisE[OF `open y`] guess N . note N = this
    1.79 -    obtain n where n: "n \<in> N" "f n \<noteq> ({}::'a set)"
    1.80 -    proof (atomize_elim, rule ccontr, clarsimp)
    1.81 -      assume "\<forall>n. n \<in> N \<longrightarrow> f n = ({}::'a set)"
    1.82 -      hence "(\<Union>n\<in>N. f n) = (\<Union>n\<in>N. {}::'a set)"
    1.83 -        by (intro UN_cong) auto
    1.84 -      hence "y = {}" unfolding N by simp
    1.85 -      with `y \<noteq> {}` show False by auto
    1.86 -    qed
    1.87 -    with x N n have "x n \<in> y" by auto
    1.88 -    thus "\<exists>n. x n \<in> y" ..
    1.89 -  qed
    1.90 -  thus ?thesis by blast
    1.91 +  let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
    1.92 +  have "countable (?f ` B)" using countable_basis by simp
    1.93 +  with basis_dense[OF is_basis, of ?f] show ?thesis
    1.94 +    by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
    1.95  qed
    1.96  
    1.97  lemma countable_dense_setE:
    1.98 -  obtains x :: "nat \<Rightarrow> 'a"
    1.99 -  where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
   1.100 -  using countable_dense_set by blast
   1.101 -
   1.102 -text {* Construction of an increasing sequence approximating open sets, therefore enumeration of
   1.103 -  basis which is closed under union. *}
   1.104 -
   1.105 -definition enum_basis::"nat \<Rightarrow> 'a set"
   1.106 -  where "enum_basis n = \<Union>(set (map f (from_nat n)))"
   1.107 -
   1.108 -lemma enum_basis_basis: "topological_basis (range enum_basis)"
   1.109 +  obtains D :: "'a set"
   1.110 +  where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
   1.111 +  using countable_dense_exists by blast
   1.112 +
   1.113 +text {* Construction of an increasing sequence approximating open sets,
   1.114 +  therefore basis which is closed under union. *}
   1.115 +
   1.116 +definition union_closed_basis::"'a set set" where
   1.117 +  "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
   1.118 +
   1.119 +lemma basis_union_closed_basis: "topological_basis union_closed_basis"
   1.120  proof (rule topological_basisI)
   1.121    fix O' and x::'a assume "open O'" "x \<in> O'"
   1.122 -  from topological_basisE[OF enumerable_basis this] guess B' . note B' = this
   1.123 -  moreover then obtain n where "B' = f n" by auto
   1.124 -  moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
   1.125 -  ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
   1.126 +  from topological_basisE[OF is_basis this] guess B' . note B' = this
   1.127 +  thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def
   1.128 +    by (auto intro!: bexI[where x="[B']"])
   1.129  next
   1.130 -  fix B' assume "B' \<in> range enum_basis"
   1.131 -  with topological_basis_open[OF enumerable_basis]
   1.132 -  show "open B'" by (auto simp add: enum_basis_def intro!: open_UN)
   1.133 -qed
   1.134 -
   1.135 -lemmas open_enum_basis = topological_basis_open[OF enum_basis_basis]
   1.136 -
   1.137 -lemma empty_basisI[intro]: "{} \<in> range enum_basis"
   1.138 -proof
   1.139 -  show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
   1.140 -qed rule
   1.141 +  fix B' assume "B' \<in> union_closed_basis"
   1.142 +  thus "open B'"
   1.143 +    using topological_basis_open[OF is_basis]
   1.144 +    by (auto simp: union_closed_basis_def)
   1.145 +qed
   1.146 +
   1.147 +lemma countable_union_closed_basis: "countable union_closed_basis"
   1.148 +  unfolding union_closed_basis_def using countable_basis by simp
   1.149 +
   1.150 +lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
   1.151 +
   1.152 +lemma union_closed_basis_ex:
   1.153 + assumes X: "X \<in> union_closed_basis"
   1.154 + shows "\<exists>B'. finite B' \<and> X = \<Union>B' \<and> B' \<subseteq> B"
   1.155 +proof -
   1.156 +  from X obtain l where "\<And>x. x\<in>set l \<Longrightarrow> x\<in>B" "X = \<Union>set l" by (auto simp: union_closed_basis_def)
   1.157 +  thus ?thesis by auto
   1.158 +qed
   1.159 +
   1.160 +lemma union_closed_basisE:
   1.161 +  assumes "X \<in> union_closed_basis"
   1.162 +  obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast
   1.163 +
   1.164 +lemma union_closed_basisI:
   1.165 +  assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B"
   1.166 +  shows "X \<in> union_closed_basis"
   1.167 +proof -
   1.168 +  from finite_list[OF `finite B'`] guess l ..
   1.169 +  thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l])
   1.170 +qed
   1.171 +
   1.172 +lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
   1.173 +  by (rule union_closed_basisI[of "{}"]) auto
   1.174  
   1.175  lemma union_basisI[intro]:
   1.176 -  assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
   1.177 -  shows "A \<union> B \<in> range enum_basis"
   1.178 -proof -
   1.179 -  from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
   1.180 -  also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
   1.181 -    by (simp add: enum_basis_def)
   1.182 -  finally show ?thesis by simp
   1.183 -qed
   1.184 +  assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis"
   1.185 +  shows "X \<union> Y \<in> union_closed_basis"
   1.186 +  using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE)
   1.187  
   1.188  lemma open_imp_Union_of_incseq:
   1.189    assumes "open X"
   1.190 -  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
   1.191 +  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis"
   1.192  proof -
   1.193 -  interpret E: enumerates_basis enum_basis proof qed (rule enum_basis_basis)
   1.194 -  from E.open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
   1.195 -  hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
   1.196 -  def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
   1.197 -    (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
   1.198 -  have S_simps[simp]:
   1.199 -    "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
   1.200 -    "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
   1.201 -    by (simp_all add: S_def)
   1.202 -  have "incseq S" by (rule incseq_SucI) auto
   1.203 -  moreover
   1.204 -  have "(\<Union>j. S j) = X" unfolding N
   1.205 -  proof safe
   1.206 -    fix x n assume "n \<in> N" "x \<in> enum_basis n"
   1.207 -    hence "x \<in> S n" by (cases n) auto
   1.208 -    thus "x \<in> (\<Union>j. S j)" by auto
   1.209 -  next
   1.210 -    fix x j
   1.211 -    assume "x \<in> S j"
   1.212 -    thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
   1.213 -  qed
   1.214 -  moreover have "range S \<subseteq> range enum_basis"
   1.215 -  proof safe
   1.216 -    fix j show "S j \<in> range enum_basis" by (induct j) auto
   1.217 -  qed
   1.218 -  ultimately show ?thesis by auto
   1.219 +  from open_countable_basis_ex[OF `open X`]
   1.220 +  obtain B' where B': "B'\<subseteq>B" "X = \<Union>B'" by auto
   1.221 +  from this(1) countable_basis have "countable B'" by (rule countable_subset)
   1.222 +  show ?thesis
   1.223 +  proof cases
   1.224 +    assume "B' \<noteq> {}"
   1.225 +    def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i"
   1.226 +    have S:"\<And>n. S n = \<Union>{from_nat_into B' i|i. i\<in>{0..n}}" unfolding S_def by force
   1.227 +    have "incseq S" by (force simp: S_def incseq_Suc_iff)
   1.228 +    moreover
   1.229 +    have "(\<Union>j. S j) = X" unfolding B'
   1.230 +    proof safe
   1.231 +      fix x X assume "X \<in> B'" "x \<in> X"
   1.232 +      then obtain n where "X = from_nat_into B' n"
   1.233 +        by (metis `countable B'` from_nat_into_surj)
   1.234 +      also have "\<dots> \<subseteq> S n" by (auto simp: S_def)
   1.235 +      finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto
   1.236 +    next
   1.237 +      fix x n
   1.238 +      assume "x \<in> S n"
   1.239 +      also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)"
   1.240 +        by (simp add: S_def)
   1.241 +      also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto
   1.242 +      also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into)
   1.243 +      finally show "x \<in> \<Union>B'" .
   1.244 +    qed
   1.245 +    moreover have "range S \<subseteq> union_closed_basis" using B'
   1.246 +      by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`)
   1.247 +    ultimately show ?thesis by auto
   1.248 +  qed (auto simp: B')
   1.249  qed
   1.250  
   1.251  lemma open_incseqE:
   1.252    assumes "open X"
   1.253 -  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
   1.254 +  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis"
   1.255    using open_imp_Union_of_incseq assms by atomize_elim
   1.256  
   1.257  end
   1.258  
   1.259 -class enumerable_basis = topological_space +
   1.260 -  assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a::topological_space set. topological_basis (range f)"
   1.261 -
   1.262 -sublocale enumerable_basis < enumerates_basis "Eps (topological_basis o range)"
   1.263 -  unfolding o_def
   1.264 -  proof qed (rule someI_ex[OF ex_enum_basis])
   1.265 +class countable_basis_space = topological_space +
   1.266 +  assumes ex_countable_basis:
   1.267 +    "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
   1.268 +
   1.269 +sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
   1.270 +  using someI_ex[OF ex_countable_basis] by unfold_locales safe
   1.271  
   1.272  subsection {* Polish spaces *}
   1.273  
   1.274  text {* Textbooks define Polish spaces as completely metrizable.
   1.275    We assume the topology to be complete for a given metric. *}
   1.276  
   1.277 -class polish_space = complete_space + enumerable_basis
   1.278 +class polish_space = complete_space + countable_basis_space
   1.279  
   1.280  subsection {* General notion of a topology as a value *}
   1.281  
   1.282 @@ -5444,35 +5457,36 @@
   1.283    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
   1.284  qed
   1.285  
   1.286 -instance ordered_euclidean_space \<subseteq> enumerable_basis
   1.287 +instance ordered_euclidean_space \<subseteq> countable_basis_space
   1.288  proof
   1.289    def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
   1.290 -  def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
   1.291 -  have "Ball (range enum) open" unfolding enum_def
   1.292 +  def B \<equiv> "(\<lambda>n. (to_cube (from_nat n)::'a set)) ` UNIV"
   1.293 +  have "countable B" unfolding B_def by simp
   1.294 +  moreover
   1.295 +  have "Ball B open" unfolding B_def
   1.296    proof safe
   1.297      fix n show "open (to_cube (from_nat n))"
   1.298        by (cases "from_nat n::rat list \<times> rat list")
   1.299           (simp add: open_interval to_cube_def)
   1.300    qed
   1.301 -  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
   1.302 +  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = x))"
   1.303    proof safe
   1.304      fix x::"'a set" assume "open x"
   1.305      def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
   1.306      from open_UNION[OF `open x`]
   1.307      have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
   1.308       by simp
   1.309 -    moreover have "to_cube ` lists \<subseteq> range enum"
   1.310 +    moreover have "to_cube ` lists \<subseteq> B"
   1.311      proof
   1.312        fix x assume "x \<in> to_cube ` lists"
   1.313        then obtain l where "l \<in> lists" "x = to_cube l" by auto
   1.314 -      hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
   1.315 -      thus "x \<in> range enum" by simp
   1.316 +      thus "x \<in> B" by (auto simp add: B_def intro!: image_eqI[where x="to_nat l"])
   1.317      qed
   1.318      ultimately
   1.319 -    show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
   1.320 +    show "\<exists>B'\<subseteq>B. \<Union>B' = x" by blast
   1.321    qed
   1.322    ultimately
   1.323 -  show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
   1.324 +  show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
   1.325  qed
   1.326  
   1.327  instance ordered_euclidean_space \<subseteq> polish_space ..