src/HOL/Probability/Essential_Supremum.thy
changeset 68751 640386ab99f3
parent 67226 ec32cdaab97b
child 69260 0a9688695a1b
equal deleted inserted replaced
68750:7087748996af 68751:640386ab99f3
   117   "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"
   117   "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"
   118 proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")
   118 proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")
   119   case True
   119   case True
   120   then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto
   120   then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto
   121   have "f x + g x \<le> esssup M f + esssup M g" if "f x \<le> esssup M f" "g x \<le> esssup M g" for x
   121   have "f x + g x \<le> esssup M f + esssup M g" if "f x \<le> esssup M f" "g x \<le> esssup M g" for x
   122     using that ereal_add_mono by auto
   122     using that add_mono by auto
   123   then have "AE x in M. f x + g x \<le> esssup M f + esssup M g"
   123   then have "AE x in M. f x + g x \<le> esssup M f + esssup M g"
   124     using esssup_AE[of f M] esssup_AE[of g M] by auto
   124     using esssup_AE[of f M] esssup_AE[of g M] by auto
   125   then show ?thesis using esssup_I by auto
   125   then show ?thesis using esssup_I by auto
   126 next
   126 next
   127   case False
   127   case False