[STATEMENT]
lemma E_sup_mono:
  "(\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> E_sup s f \<le> E_sup s g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> E_sup s f \<le> E_sup s g
[PROOF STEP]
unfolding E_sup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> (\<Squnion>cfg\<in>cfg_on s. integral\<^sup>N (T cfg) f) \<le> (\<Squnion>cfg\<in>cfg_on s. integral\<^sup>N (T cfg) g)
[PROOF STEP]
by (intro SUP_subset_mono order_refl nn_integral_mono)