renamed countable_basis_space to second_countable_topology
authorhoelzl
Mon Jan 14 17:29:04 2013 +0100 (2013-01-14)
changeset 50881ae630bab13da
parent 50880 b22ecedde1c7
child 50882 a382bf90867e
renamed countable_basis_space to second_countable_topology
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Discrete_Topology.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Regularity.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:16:59 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:29:04 2013 +0100
     1.3 @@ -220,11 +220,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class countable_basis_space = topological_space +
     1.8 +class second_countable_topology = topological_space +
     1.9    assumes ex_countable_basis:
    1.10      "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
    1.11  
    1.12 -sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
    1.13 +sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
    1.14    using someI_ex[OF ex_countable_basis] by unfold_locales safe
    1.15  
    1.16  subsection {* Polish spaces *}
    1.17 @@ -232,7 +232,7 @@
    1.18  text {* Textbooks define Polish spaces as completely metrizable.
    1.19    We assume the topology to be complete for a given metric. *}
    1.20  
    1.21 -class polish_space = complete_space + countable_basis_space
    1.22 +class polish_space = complete_space + second_countable_topology
    1.23  
    1.24  subsection {* General notion of a topology as a value *}
    1.25  
    1.26 @@ -5411,7 +5411,7 @@
    1.27    finally show ?thesis .
    1.28  qed
    1.29  
    1.30 -instance euclidean_space \<subseteq> countable_basis_space
    1.31 +instance euclidean_space \<subseteq> second_countable_topology
    1.32  proof
    1.33    def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
    1.34    then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:16:59 2013 +0100
     2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 17:29:04 2013 +0100
     2.3 @@ -172,7 +172,7 @@
     2.4    qed auto
     2.5  qed (metis A B topological_basis_open open_Times)
     2.6  
     2.7 -instance prod :: (countable_basis_space, countable_basis_space) countable_basis_space
     2.8 +instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
     2.9  proof
    2.10    obtain A :: "'a set set" where "countable A" "topological_basis A"
    2.11      using ex_countable_basis by auto
    2.12 @@ -184,7 +184,7 @@
    2.13  qed
    2.14  
    2.15  lemma borel_measurable_Pair[measurable (raw)]:
    2.16 -  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
    2.17 +  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
    2.18    assumes f[measurable]: "f \<in> borel_measurable M"
    2.19    assumes g[measurable]: "g \<in> borel_measurable M"
    2.20    shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
    2.21 @@ -257,7 +257,7 @@
    2.22  qed
    2.23  
    2.24  lemma borel_measurable_continuous_Pair:
    2.25 -  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
    2.26 +  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
    2.27    assumes [measurable]: "f \<in> borel_measurable M"
    2.28    assumes [measurable]: "g \<in> borel_measurable M"
    2.29    assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
    2.30 @@ -271,7 +271,7 @@
    2.31  section "Borel spaces on euclidean spaces"
    2.32  
    2.33  lemma borel_measurable_inner[measurable (raw)]:
    2.34 -  fixes f g :: "'a \<Rightarrow> 'b::{countable_basis_space, real_inner}"
    2.35 +  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
    2.36    assumes "f \<in> borel_measurable M"
    2.37    assumes "g \<in> borel_measurable M"
    2.38    shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
     3.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:16:59 2013 +0100
     3.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:29:04 2013 +0100
     3.3 @@ -48,7 +48,7 @@
     3.4    thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
     3.5  qed
     3.6  
     3.7 -instance discrete :: (countable) countable_basis_space
     3.8 +instance discrete :: (countable) second_countable_topology
     3.9  proof
    3.10    let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    3.11    have "topological_basis ?B"
     4.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:16:59 2013 +0100
     4.2 +++ b/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 17:29:04 2013 +0100
     4.3 @@ -1045,7 +1045,7 @@
     4.4  lemma product_open_generates_sets_PiF_single:
     4.5    assumes "I \<noteq> {}"
     4.6    assumes [simp]: "finite I"
     4.7 -  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
     4.8 +  shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
     4.9      sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
    4.10  proof -
    4.11    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
    4.12 @@ -1064,7 +1064,7 @@
    4.13  lemma product_open_generates_sets_PiM:
    4.14    assumes "I \<noteq> {}"
    4.15    assumes [simp]: "finite I"
    4.16 -  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
    4.17 +  shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
    4.18      sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
    4.19  proof -
    4.20    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
     5.1 --- a/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:16:59 2013 +0100
     5.2 +++ b/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:29:04 2013 +0100
     5.3 @@ -104,7 +104,7 @@
     5.4  qed
     5.5  
     5.6  lemma
     5.7 -  fixes M::"'a::{countable_basis_space, complete_space} measure"
     5.8 +  fixes M::"'a::{second_countable_topology, complete_space} measure"
     5.9    assumes sb: "sets M = sets borel"
    5.10    assumes "emeasure M (space M) \<noteq> \<infinity>"
    5.11    assumes "B \<in> sets borel"