--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jan 14 17:29:04 2013 +0100
@@ -220,11 +220,11 @@
end
-class countable_basis_space = topological_space +
+class second_countable_topology = topological_space +
assumes ex_countable_basis:
"\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
-sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
+sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
using someI_ex[OF ex_countable_basis] by unfold_locales safe
subsection {* Polish spaces *}
@@ -232,7 +232,7 @@
text {* Textbooks define Polish spaces as completely metrizable.
We assume the topology to be complete for a given metric. *}
-class polish_space = complete_space + countable_basis_space
+class polish_space = complete_space + second_countable_topology
subsection {* General notion of a topology as a value *}
@@ -5411,7 +5411,7 @@
finally show ?thesis .
qed
-instance euclidean_space \<subseteq> countable_basis_space
+instance euclidean_space \<subseteq> second_countable_topology
proof
def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
--- a/src/HOL/Probability/Borel_Space.thy Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Mon Jan 14 17:29:04 2013 +0100
@@ -172,7 +172,7 @@
qed auto
qed (metis A B topological_basis_open open_Times)
-instance prod :: (countable_basis_space, countable_basis_space) countable_basis_space
+instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
proof
obtain A :: "'a set set" where "countable A" "topological_basis A"
using ex_countable_basis by auto
@@ -184,7 +184,7 @@
qed
lemma borel_measurable_Pair[measurable (raw)]:
- fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+ fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
assumes f[measurable]: "f \<in> borel_measurable M"
assumes g[measurable]: "g \<in> borel_measurable M"
shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
@@ -257,7 +257,7 @@
qed
lemma borel_measurable_continuous_Pair:
- fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+ fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
assumes [measurable]: "f \<in> borel_measurable M"
assumes [measurable]: "g \<in> borel_measurable M"
assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
@@ -271,7 +271,7 @@
section "Borel spaces on euclidean spaces"
lemma borel_measurable_inner[measurable (raw)]:
- fixes f g :: "'a \<Rightarrow> 'b::{countable_basis_space, real_inner}"
+ fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
assumes "f \<in> borel_measurable M"
assumes "g \<in> borel_measurable M"
shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
--- a/src/HOL/Probability/Discrete_Topology.thy Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Mon Jan 14 17:29:04 2013 +0100
@@ -48,7 +48,7 @@
thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
qed
-instance discrete :: (countable) countable_basis_space
+instance discrete :: (countable) second_countable_topology
proof
let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
have "topological_basis ?B"
--- a/src/HOL/Probability/Fin_Map.thy Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Mon Jan 14 17:29:04 2013 +0100
@@ -1045,7 +1045,7 @@
lemma product_open_generates_sets_PiF_single:
assumes "I \<noteq> {}"
assumes [simp]: "finite I"
- shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
+ shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
proof -
from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
@@ -1064,7 +1064,7 @@
lemma product_open_generates_sets_PiM:
assumes "I \<noteq> {}"
assumes [simp]: "finite I"
- shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
+ shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
proof -
from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
--- a/src/HOL/Probability/Regularity.thy Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy Mon Jan 14 17:29:04 2013 +0100
@@ -104,7 +104,7 @@
qed
lemma
- fixes M::"'a::{countable_basis_space, complete_space} measure"
+ fixes M::"'a::{second_countable_topology, complete_space} measure"
assumes sb: "sets M = sets borel"
assumes "emeasure M (space M) \<noteq> \<infinity>"
assumes "B \<in> sets borel"