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.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.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.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.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.102 -text {* Construction of an increasing sequence approximating open sets, therefore enumeration of
1.103 -  basis which is closed under union. *}
1.105 -definition enum_basis::"nat \<Rightarrow> 'a set"
1.106 -  where "enum_basis n = \<Union>(set (map f (from_nat n)))"
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.113 +text {* Construction of an increasing sequence approximating open sets,
1.114 +  therefore basis which is closed under union. *}
1.116 +definition union_closed_basis::"'a set set" where
1.117 +  "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
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.135 -lemmas open_enum_basis = topological_basis_open[OF enum_basis_basis]
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.147 +lemma countable_union_closed_basis: "countable union_closed_basis"
1.148 +  unfolding union_closed_basis_def using countable_basis by simp
1.150 +lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
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.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.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.172 +lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
1.173 +  by (rule union_closed_basisI[of "{}"]) auto
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.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.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.257  end
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.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.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.272  subsection {* Polish spaces *}
1.274  text {* Textbooks define Polish spaces as completely metrizable.
1.275    We assume the topology to be complete for a given metric. *}
1.277 -class polish_space = complete_space + enumerable_basis
1.278 +class polish_space = complete_space + countable_basis_space
1.280  subsection {* General notion of a topology as a value *}
1.282 @@ -5444,35 +5457,36 @@
1.283    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.284  qed
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.327  instance ordered_euclidean_space \<subseteq> polish_space ..