655 by (auto simp add: sigma_def intro!: sigma_sets.Basic) } |
655 by (auto simp add: sigma_def intro!: sigma_sets.Basic) } |
656 then show ?thesis |
656 then show ?thesis |
657 unfolding borel_def by (intro sets_sigma_subset) auto |
657 unfolding borel_def by (intro sets_sigma_subset) auto |
658 qed |
658 qed |
659 qed auto |
659 qed auto |
|
660 |
|
661 lemma borel_eq_atLeastLessThan: |
|
662 "borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S") |
|
663 proof (intro algebra.equality antisym) |
|
664 interpret sigma_algebra ?S |
|
665 by (rule sigma_algebra_sigma) auto |
|
666 show "sets borel \<subseteq> sets ?S" |
|
667 unfolding borel_eq_lessThan |
|
668 proof (intro sets_sigma_subset subsetI) |
|
669 have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto |
|
670 fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>" |
|
671 then obtain x where "A = {..< x}" by auto |
|
672 then have "A = (\<Union>i::nat. {-real i ..< x})" |
|
673 by (auto simp: move_uminus real_arch_simple) |
|
674 then show "A \<in> sets ?S" |
|
675 by (auto simp: sets_sigma intro!: sigma_sets.intros) |
|
676 qed simp |
|
677 show "sets ?S \<subseteq> sets borel" |
|
678 by (intro borel.sets_sigma_subset) auto |
|
679 qed simp_all |
660 |
680 |
661 lemma borel_eq_halfspace_le: |
681 lemma borel_eq_halfspace_le: |
662 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)" |
682 "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)" |
663 (is "_ = ?SIGMA") |
683 (is "_ = ?SIGMA") |
664 proof (intro algebra.equality antisym) |
684 proof (intro algebra.equality antisym) |