diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Wed Dec 08 16:15:14 2010 +0100 +++ b/src/HOL/Probability/Borel_Space.thy Wed Dec 08 19:32:11 2010 +0100 @@ -1395,7 +1395,7 @@ lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]: fixes f :: "'d\countable \ 'a \ pextreal" assumes "\i. i \ A \ f i \ borel_measurable M" - shows "(SUP i : A. f i) \ borel_measurable M" (is "?sup \ borel_measurable M") + shows "(\x. SUP i : A. f i x) \ borel_measurable M" (is "?sup \ borel_measurable M") unfolding borel_measurable_pextreal_iff_greater proof safe fix a @@ -1408,7 +1408,7 @@ lemma (in sigma_algebra) borel_measurable_INF[simp, intro]: fixes f :: "'d :: countable \ 'a \ pextreal" assumes "\i. i \ A \ f i \ borel_measurable M" - shows "(INF i : A. f i) \ borel_measurable M" (is "?inf \ borel_measurable M") + shows "(\x. INF i : A. f i x) \ borel_measurable M" (is "?inf \ borel_measurable M") unfolding borel_measurable_pextreal_iff_less proof safe fix a @@ -1432,20 +1432,10 @@ using assms by auto qed -lemma INFI_fun_expand: - "(INF y:A. f y) = (\x. (INF y:A. f y x))" - by (simp add: fun_eq_iff INFI_apply) - -lemma SUPR_fun_expand: - "(SUP y:A. f y) = (\x. (SUP y:A. f y x))" - by (simp add: fun_eq_iff SUPR_apply) - lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]: assumes "\i. f i \ borel_measurable M" shows "(\x. (\\<^isub>\ i. f i x)) \ borel_measurable M" - using assms unfolding psuminf_def - by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand]) - + using assms unfolding psuminf_def by auto section "LIMSEQ is borel measurable" @@ -1468,13 +1458,12 @@ note eq = this have *: "\x. real (Real (u' x)) - real (Real (- u' x)) = u' x" by auto - have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M" - "(SUP n. INF m. (\x. Real (- u (n + m) x))) \ borel_measurable M" - using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) + have "(\x. SUP n. INF m. Real (u (n + m) x)) \ borel_measurable M" + "(\x. SUP n. INF m. Real (- u (n + m) x)) \ borel_measurable M" + using u by auto with eq[THEN measurable_cong, of M "\x. x" borel] have "(\x. Real (u' x)) \ borel_measurable M" - "(\x. Real (- u' x)) \ borel_measurable M" - unfolding SUPR_fun_expand INFI_fun_expand by auto + "(\x. Real (- u' x)) \ borel_measurable M" by auto note this[THEN borel_measurable_real] from borel_measurable_diff[OF this] show ?thesis unfolding * .