src/HOL/Probability/Borel_Space.thy

     by (rule sigma_sets.Compl)
        (auto intro!: sigma_sets.Basic simp: `closed x`)
   finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
 qed simp_all
 
-lemma borel_eq_enumerated_basis:
-  fixes f::"nat\<Rightarrow>'a::topological_space set"
-  assumes "topological_basis (range f)"
-  shows "borel = sigma UNIV (range f)"
+lemma borel_eq_countable_basis:
+  fixes B::"'a::topological_space set set"
+  assumes "countable B"
+  assumes "topological_basis B"
+  shows "borel = sigma UNIV B"
   unfolding borel_def
 proof (intro sigma_eqI sigma_sets_eqI, safe)
-  interpret enumerates_basis proof qed (rule assms)
-  fix x::"'a set" assume "open x"
-  from open_enumerable_basisE[OF this] guess N .
-  hence x: "x = (\<Union>n. if n \<in> N then f n else {})" by (auto split: split_if_asm)
-  also have "\<dots> \<in> sigma_sets UNIV (range f)" by (auto intro!: sigma_sets.Empty Union)
-  finally show "x \<in> sigma_sets UNIV (range f)" .
+  interpret countable_basis using assms by unfold_locales
+  fix X::"'a set" assume "open X"
+  from open_countable_basisE[OF this] guess B' . note B' = this
+  show "X \<in> sigma_sets UNIV B"
+  proof cases
+    assume "B' \<noteq> {}"
+    thus "X \<in> sigma_sets UNIV B" using assms B'
+      by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into
+        in_mono sigma_sets.Basic sigma_sets.Union)
+  qed (simp add: sigma_sets.Empty B')
 next
-  fix n
-  have "open (f n)" by (rule topological_basis_open[OF assms]) simp
-  thus "f n \<in> sigma_sets UNIV (Collect open)" by auto
+  fix b assume "b \<in> B"
+  hence "open b" by (rule topological_basis_open[OF assms(2)])
+  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
 qed simp_all
 
-lemma borel_eq_enum_basis:
-  "borel = sigma UNIV (range enum_basis)"
-  by (rule borel_eq_enumerated_basis[OF enum_basis_basis])
+lemma borel_eq_union_closed_basis:
+  "borel = sigma UNIV union_closed_basis"
+  by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
 
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
   assumes F: "borel = sigma UNIV (range F)"
   and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M"