move prod instantiation of second_countable_topology to its definition
authorhoelzl
Mon Jan 14 17:30:36 2013 +0100 (2013-01-14)
changeset 50882a382bf90867e
parent 50881 ae630bab13da
child 50883 1421884baf5b
move prod instantiation of second_countable_topology to its definition
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:29:04 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:30:36 2013 +0100
     1.3 @@ -93,6 +93,25 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma topological_basis_prod:
     1.8 +  assumes A: "topological_basis A" and B: "topological_basis B"
     1.9 +  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
    1.10 +  unfolding topological_basis_def
    1.11 +proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
    1.12 +  fix S :: "('a \<times> 'b) set" assume "open S"
    1.13 +  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
    1.14 +  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
    1.15 +    fix x y assume "(x, y) \<in> S"
    1.16 +    from open_prod_elim[OF `open S` this]
    1.17 +    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
    1.18 +      by (metis mem_Sigma_iff)
    1.19 +    moreover from topological_basisE[OF A a] guess A0 .
    1.20 +    moreover from topological_basisE[OF B b] guess B0 .
    1.21 +    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
    1.22 +      by (intro UN_I[of "(A0, B0)"]) auto
    1.23 +  qed auto
    1.24 +qed (metis A B topological_basis_open open_Times)
    1.25 +
    1.26  subsection {* Countable Basis *}
    1.27  
    1.28  locale countable_basis =
    1.29 @@ -227,6 +246,17 @@
    1.30  sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
    1.31    using someI_ex[OF ex_countable_basis] by unfold_locales safe
    1.32  
    1.33 +instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
    1.34 +proof
    1.35 +  obtain A :: "'a set set" where "countable A" "topological_basis A"
    1.36 +    using ex_countable_basis by auto
    1.37 +  moreover
    1.38 +  obtain B :: "'b set set" where "countable B" "topological_basis B"
    1.39 +    using ex_countable_basis by auto
    1.40 +  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
    1.41 +    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
    1.42 +qed
    1.43 +
    1.44  subsection {* Polish spaces *}
    1.45  
    1.46  text {* Textbooks define Polish spaces as completely metrizable.
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:29:04 2013 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:30:36 2013 +0100
     2.3 @@ -153,36 +153,6 @@
     2.4    "borel = sigma UNIV union_closed_basis"
     2.5    by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
     2.6  
     2.7 -lemma topological_basis_prod:
     2.8 -  assumes A: "topological_basis A" and B: "topological_basis B"
     2.9 -  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
    2.10 -  unfolding topological_basis_def
    2.11 -proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
    2.12 -  fix S :: "('a \<times> 'b) set" assume "open S"
    2.13 -  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
    2.14 -  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
    2.15 -    fix x y assume "(x, y) \<in> S"
    2.16 -    from open_prod_elim[OF `open S` this]
    2.17 -    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
    2.18 -      by (metis mem_Sigma_iff)
    2.19 -    moreover from topological_basisE[OF A a] guess A0 .
    2.20 -    moreover from topological_basisE[OF B b] guess B0 .
    2.21 -    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
    2.22 -      by (intro UN_I[of "(A0, B0)"]) auto
    2.23 -  qed auto
    2.24 -qed (metis A B topological_basis_open open_Times)
    2.25 -
    2.26 -instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
    2.27 -proof
    2.28 -  obtain A :: "'a set set" where "countable A" "topological_basis A"
    2.29 -    using ex_countable_basis by auto
    2.30 -  moreover
    2.31 -  obtain B :: "'b set set" where "countable B" "topological_basis B"
    2.32 -    using ex_countable_basis by auto
    2.33 -  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
    2.34 -    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
    2.35 -qed
    2.36 -
    2.37  lemma borel_measurable_Pair[measurable (raw)]:
    2.38    fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
    2.39    assumes f[measurable]: "f \<in> borel_measurable M"