src/HOL/Probability/Borel_Space.thy
changeset 42862 7d7627738e66
parent 42150 b0c0638c4aad
child 42950 6e5c2a3c69da
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue May 17 11:47:36 2011 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue May 17 12:21:58 2011 +0200
     1.3 @@ -658,6 +658,26 @@
     1.4    qed
     1.5  qed auto
     1.6  
     1.7 +lemma borel_eq_atLeastLessThan:
     1.8 +  "borel = sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real})\<rparr>" (is "_ = ?S")
     1.9 +proof (intro algebra.equality antisym)
    1.10 +  interpret sigma_algebra ?S
    1.11 +    by (rule sigma_algebra_sigma) auto
    1.12 +  show "sets borel \<subseteq> sets ?S"
    1.13 +    unfolding borel_eq_lessThan
    1.14 +  proof (intro sets_sigma_subset subsetI)
    1.15 +    have move_uminus: "\<And>x y::real. -x \<le> y \<longleftrightarrow> -y \<le> x" by auto
    1.16 +    fix A :: "real set" assume "A \<in> sets \<lparr>space = UNIV, sets = range lessThan\<rparr>"
    1.17 +    then obtain x where "A = {..< x}" by auto
    1.18 +    then have "A = (\<Union>i::nat. {-real i ..< x})"
    1.19 +      by (auto simp: move_uminus real_arch_simple)
    1.20 +    then show "A \<in> sets ?S"
    1.21 +      by (auto simp: sets_sigma intro!: sigma_sets.intros)
    1.22 +  qed simp
    1.23 +  show "sets ?S \<subseteq> sets borel"
    1.24 +    by (intro borel.sets_sigma_subset) auto
    1.25 +qed simp_all
    1.26 +
    1.27  lemma borel_eq_halfspace_le:
    1.28    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
    1.29     (is "_ = ?SIGMA")