src/HOL/Probability/Discrete_Topology.thy
changeset 50245 dea9363887a6
parent 50089 1badf63e5d97
child 50881 ae630bab13da
     1.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -48,15 +48,17 @@
     1.4    thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
     1.5  qed
     1.6  
     1.7 -instance discrete :: (countable) enumerable_basis
     1.8 +instance discrete :: (countable) countable_basis_space
     1.9  proof
    1.10 -  have "topological_basis (range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    1.11 +  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    1.12 +  have "topological_basis ?B"
    1.13    proof (intro topological_basisI)
    1.14      fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
    1.15      thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
    1.16        by (auto intro: exI[where x="to_nat x"])
    1.17    qed (simp add: open_discrete_def)
    1.18 -  thus "\<exists>f::nat\<Rightarrow>'a discrete set. topological_basis (range f)" by blast
    1.19 +  moreover have "countable ?B" by simp
    1.20 +  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
    1.21  qed
    1.22  
    1.23  instance discrete :: (countable) polish_space ..