src/HOL/Probability/Borel.thy

 definition indicator_fn where
   "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
 
 definition mono_convergent where
   "mono_convergent u f s \<equiv>
-	(\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
-	(\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+        (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
 
 lemma in_borel_measurable:
    "f \<in> borel_measurable M \<longleftrightarrow>
     sigma_algebra M \<and>
     (\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))).

   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
 proof -
   have "{w \<in> space M. f w < g w} =
-	(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+        (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
     by (auto simp add: Rats_dense_in_real)
   thus ?thesis using f g 
     by (simp add: borel_measurable_less_iff [of f]  
                   borel_measurable_gr_iff [of g]) 
        (blast intro: gen_countable_UN [OF rats_enumeration])

   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w = g w} \<in> sets M"
 proof -
   have "{w \<in> space M. f w = g w} =
-	{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
     by auto
   thus ?thesis using f g 
     by (simp add: borel_measurable_leq_borel_measurable Int) 
 qed