# HG changeset patch # User nipkow # Date 1531300586 -7200 # Node ID 640386ab99f3dec93edfa0662825c0e6b16a6fa2 # Parent 7087748996af6a01ccf2f9c6aec7ca53c0e9e41e updated to renaming diff -r 7087748996af -r 640386ab99f3 src/HOL/Probability/Essential_Supremum.thy --- a/src/HOL/Probability/Essential_Supremum.thy Wed Aug 15 16:09:44 2018 +0200 +++ b/src/HOL/Probability/Essential_Supremum.thy Wed Jul 11 11:16:26 2018 +0200 @@ -119,7 +119,7 @@ case True then have [measurable]: "(\x. f x + g x) \ borel_measurable M" by auto have "f x + g x \ esssup M f + esssup M g" if "f x \ esssup M f" "g x \ esssup M g" for x - using that ereal_add_mono by auto + using that add_mono by auto then have "AE x in M. f x + g x \ esssup M f + esssup M g" using esssup_AE[of f M] esssup_AE[of g M] by auto then show ?thesis using esssup_I by auto