454 by (rule sigma_sets.Compl) |
454 by (rule sigma_sets.Compl) |
455 (auto intro!: sigma_sets.Basic simp: `closed x`) |
455 (auto intro!: sigma_sets.Basic simp: `closed x`) |
456 finally show "x \<in> sigma_sets UNIV (Collect open)" by simp |
456 finally show "x \<in> sigma_sets UNIV (Collect open)" by simp |
457 qed simp_all |
457 qed simp_all |
458 |
458 |
|
459 lemma borel_eq_enumerated_basis: |
|
460 fixes f::"nat\<Rightarrow>'a::topological_space set" |
|
461 assumes "topological_basis (range f)" |
|
462 shows "borel = sigma UNIV (range f)" |
|
463 unfolding borel_def |
|
464 proof (intro sigma_eqI sigma_sets_eqI, safe) |
|
465 interpret enumerates_basis proof qed (rule assms) |
|
466 fix x::"'a set" assume "open x" |
|
467 from open_enumerable_basisE[OF this] guess N . |
|
468 hence x: "x = (\<Union>n. if n \<in> N then f n else {})" by (auto split: split_if_asm) |
|
469 also have "\<dots> \<in> sigma_sets UNIV (range f)" by (auto intro!: sigma_sets.Empty Union) |
|
470 finally show "x \<in> sigma_sets UNIV (range f)" . |
|
471 next |
|
472 fix n |
|
473 have "open (f n)" by (rule topological_basis_open[OF assms]) simp |
|
474 thus "f n \<in> sigma_sets UNIV (Collect open)" by auto |
|
475 qed simp_all |
|
476 |
459 lemma borel_eq_enum_basis: |
477 lemma borel_eq_enum_basis: |
460 "borel = sigma UNIV (range enum_basis)" |
478 "borel = sigma UNIV (range enum_basis)" |
461 unfolding borel_def |
479 by (rule borel_eq_enumerated_basis[OF enum_basis_basis]) |
462 proof (intro sigma_eqI sigma_sets_eqI, safe) |
|
463 fix x::"'a set" assume "open x" |
|
464 from open_enumerable_basisE[OF this] guess N . |
|
465 hence x: "x = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm) |
|
466 also have "\<dots> \<in> sigma_sets UNIV (range enum_basis)" by (rule Union) auto |
|
467 finally show "x \<in> sigma_sets UNIV (range enum_basis)" . |
|
468 next |
|
469 fix n |
|
470 have "open (enum_basis n)" by (rule open_enum_basis) simp |
|
471 thus "enum_basis n \<in> sigma_sets UNIV (Collect open)" by auto |
|
472 qed simp_all |
|
473 |
480 |
474 lemma borel_measurable_halfspacesI: |
481 lemma borel_measurable_halfspacesI: |
475 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
482 fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space" |
476 assumes F: "borel = sigma UNIV (range F)" |
483 assumes F: "borel = sigma UNIV (range F)" |
477 and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" |
484 and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" |