src/HOL/Probability/Radon_Nikodym.thy
changeset 41097 a1abfa4e2b44
parent 41095 c335d880ff82
child 41544 c3b977fee8a3
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 16:15:14 2010 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 19:32:11 2010 +0100
     1.3 @@ -323,9 +323,10 @@
     1.4    { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
     1.5      have "g \<in> G" unfolding G_def
     1.6      proof safe
     1.7 -      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
     1.8 +      from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
     1.9 +        unfolding isoton_def fun_eq_iff SUPR_apply by simp
    1.10        have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
    1.11 -      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
    1.12 +      thus "g \<in> borel_measurable M" by auto
    1.13        fix A assume "A \<in> sets M"
    1.14        hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
    1.15          using f_borel by (auto intro!: borel_measurable_indicator)