[STATEMENT]
lemma emeasure_lborel_box_eq:
  "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure lborel (box l u) = ennreal (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then prod ((\<bullet>) (u - l)) Basis else 0)
[PROOF STEP]
using box_eq_empty(1)[THEN iffD2, of u l]
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>Basis. u \<bullet> i \<le> l \<bullet> i \<Longrightarrow> box l u = {}

goal (1 subgoal):
 1. emeasure lborel (box l u) = ennreal (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then prod ((\<bullet>) (u - l)) Basis else 0)
[PROOF STEP]
by (auto simp: not_le dest!: less_imp_le) force