src/HOL/Probability/Discrete_Topology.thy
changeset 51343 b61b32f62c78
parent 51000 c9adb50f74ad
child 61808 fc1556774cfe
     1.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:13 2013 +0100
     1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 15:43:14 2013 +0100
     1.3 @@ -50,15 +50,13 @@
     1.4  
     1.5  instance discrete :: (countable) second_countable_topology
     1.6  proof
     1.7 -  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
     1.8 -  have "topological_basis ?B"
     1.9 -  proof (intro topological_basisI)
    1.10 -    fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
    1.11 -    thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
    1.12 -      by (auto intro: exI[where x="to_nat x"])
    1.13 -  qed (simp add: open_discrete_def)
    1.14 +  let ?B = "range (\<lambda>n::'a discrete. {n})"
    1.15 +  have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
    1.16 +    by (intro generate_topology_Union) (auto intro: generate_topology.intros)
    1.17 +  then have "open = generate_topology ?B"
    1.18 +    by (auto intro!: ext simp: open_discrete_def)
    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 +  ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
    1.22  qed
    1.23  
    1.24  instance discrete :: (countable) polish_space ..