src/HOL/Probability/Bochner_Integration.thy

                  simp del: norm_scaleR
                  split: split_indicator)
     qed
   qed
 qed (simp add: integrable_restrict_space)
+
+lemma integral_empty:
+  assumes "space M = {}"
+  shows "integral\<^sup>L M f = 0"
+proof -
+  have "(\<integral> x. f x \<partial>M) = (\<integral> x. 0 \<partial>M)"
+    by(rule integral_cong)(simp_all add: assms)
+  thus ?thesis by simp
+qed
 
 subsection {* Measure spaces with an associated density *}
 
 lemma integrable_density:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"