use generate_topology for second countable topologies, does not require intersection stable basis
authorhoelzl
Tue Mar 05 15:43:14 2013 +0100 (2013-03-05)
changeset 51343b61b32f62c78
parent 51342 763c6872bd10
child 51344 b3d246c92dfb
use generate_topology for second countable topologies, does not require intersection stable basis
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Discrete_Topology.thy
src/HOL/Probability/Fin_Map.thy
     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