author hoelzl Tue Mar 05 15:43:14 2013 +0100 (2013-03-05) changeset 51343 b61b32f62c78 parent 51342 763c6872bd10 child 51344 b3d246c92dfb
use generate_topology for second countable topologies, does not require intersection stable basis
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:13 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:14 2013 +0100
1.3 @@ -40,9 +40,10 @@
1.4  begin
1.5
1.6  definition "topological_basis B =
1.7 -  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
1.8 -
1.9 -lemma "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x))"
1.10 +  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))"
1.11 +
1.12 +lemma topological_basis:
1.13 +  "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
1.14    unfolding topological_basis_def
1.15    apply safe
1.16       apply fastforce
1.17 @@ -100,6 +101,19 @@
1.18    using assms
1.19    by (simp add: topological_basis_def)
1.20
1.21 +lemma topological_basis_imp_subbasis:
1.22 +  assumes B: "topological_basis B" shows "open = generate_topology B"
1.23 +proof (intro ext iffI)
1.24 +  fix S :: "'a set" assume "open S"
1.25 +  with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
1.26 +    unfolding topological_basis_def by blast
1.27 +  then show "generate_topology B S"
1.28 +    by (auto intro: generate_topology.intros dest: topological_basis_open)
1.29 +next
1.30 +  fix S :: "'a set" assume "generate_topology B S" then show "open S"
1.31 +    by induct (auto dest: topological_basis_open[OF B])
1.32 +qed
1.33 +
1.34  lemma basis_dense:
1.35    fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
1.36    assumes "topological_basis B"
1.37 @@ -269,11 +283,56 @@
1.38  qed
1.39
1.40  class second_countable_topology = topological_space +
1.41 -  assumes ex_countable_basis:
1.42 -    "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
1.43 -
1.44 -sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
1.45 -  using someI_ex[OF ex_countable_basis] by unfold_locales safe
1.46 +  assumes ex_countable_subbasis: "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B"
1.47 +begin
1.48 +
1.49 +lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
1.50 +proof -
1.51 +  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast
1.52 +  let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
1.53 +
1.54 +  show ?thesis
1.55 +  proof (intro exI conjI)
1.56 +    show "countable ?B"
1.57 +      by (intro countable_image countable_Collect_finite_subset B)
1.58 +    { fix S assume "open S"
1.59 +      then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
1.60 +        unfolding B
1.61 +      proof induct
1.62 +        case UNIV show ?case by (intro exI[of _ "{{}}"]) simp
1.63 +      next
1.64 +        case (Int a b)
1.65 +        then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
1.66 +          and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
1.67 +          by blast
1.68 +        show ?case
1.69 +          unfolding x y Int_UN_distrib2
1.70 +          by (intro exI[of _ "{i \<union> j| i j.  i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
1.71 +      next
1.72 +        case (UN K)
1.73 +        then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
1.74 +        then guess k unfolding bchoice_iff ..
1.75 +        then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
1.76 +          by (intro exI[of _ "UNION K k"]) auto
1.77 +      next
1.78 +        case (Basis S) then show ?case
1.79 +          by (intro exI[of _ "{{S}}"]) auto
1.80 +      qed
1.81 +      then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
1.82 +        unfolding subset_image_iff by blast }
1.83 +    then show "topological_basis ?B"
1.84 +      unfolding topological_space_class.topological_basis_def
1.85 +      by (safe intro!: topological_space_class.open_Inter)
1.86 +         (simp_all add: B generate_topology.Basis subset_eq)
1.87 +  qed
1.88 +qed
1.89 +
1.90 +end
1.91 +
1.92 +sublocale second_countable_topology <
1.93 +  countable_basis "SOME B. countable B \<and> topological_basis B"
1.94 +  using someI_ex[OF ex_countable_basis]
1.95 +  by unfold_locales safe
1.96
1.97  instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
1.98  proof
1.99 @@ -282,8 +341,9 @@
1.100    moreover
1.101    obtain B :: "'b set set" where "countable B" "topological_basis B"
1.102      using ex_countable_basis by auto
1.103 -  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
1.104 -    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
1.105 +  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B"
1.106 +    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod
1.107 +      topological_basis_imp_subbasis)
1.108  qed
1.109
1.110  instance second_countable_topology \<subseteq> first_countable_topology
1.111 @@ -5706,9 +5766,6 @@
1.112    then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f" by simp
1.113    def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^isub>E (\<rat> \<times> \<rat>))"
1.114
1.115 -  have "countable B" unfolding B_def
1.116 -    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
1.117 -  moreover
1.118    have "Ball B open" by (simp add: B_def open_box)
1.119    moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
1.120    proof safe
1.121 @@ -5720,7 +5777,12 @@
1.122        done
1.123    qed
1.124    ultimately
1.125 -  show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
1.126 +  have "topological_basis B" unfolding topological_basis_def by blast
1.127 +  moreover
1.128 +  have "countable B" unfolding B_def
1.129 +    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
1.130 +  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
1.131 +    by (blast intro: topological_basis_imp_subbasis)
1.132  qed
1.133
1.134  instance euclidean_space \<subseteq> polish_space ..
```
```     2.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:13 2013 +0100
2.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:14 2013 +0100
2.3 @@ -50,15 +50,13 @@
2.4
2.5  instance discrete :: (countable) second_countable_topology
2.6  proof
2.7 -  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
2.8 -  have "topological_basis ?B"
2.9 -  proof (intro topological_basisI)
2.10 -    fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
2.11 -    thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
2.12 -      by (auto intro: exI[where x="to_nat x"])
2.13 -  qed (simp add: open_discrete_def)
2.14 +  let ?B = "range (\<lambda>n::'a discrete. {n})"
2.15 +  have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
2.16 +    by (intro generate_topology_Union) (auto intro: generate_topology.intros)
2.17 +  then have "open = generate_topology ?B"
2.18 +    by (auto intro!: ext simp: open_discrete_def)
2.19    moreover have "countable ?B" by simp
2.20 -  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
2.21 +  ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
2.22  qed
2.23
2.24  instance discrete :: (countable) polish_space ..
```
```     3.1 --- a/src/HOL/Probability/Fin_Map.thy	Tue Mar 05 15:43:13 2013 +0100
3.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Mar 05 15:43:14 2013 +0100
3.3 @@ -605,7 +605,7 @@
3.4    shows "open x"
3.5    using finmap_topological_basis assms by (auto simp: topological_basis_def)
3.6
3.7 -instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap)
3.8 +instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap topological_basis_imp_subbasis)
3.9
3.10  end
3.11
```