src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50881 ae630bab13da
parent 50526 899c9c4e4a4c
child 50882 a382bf90867e
     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