--- a/src/HOL/Analysis/Binary_Product_Measure.thy Wed Feb 01 23:02:59 2023 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Thu Feb 02 12:55:07 2023 +0000
@@ -340,6 +340,16 @@
by (simp add: ac_simps)
qed
+lemma (in sigma_finite_measure) times_in_null_sets1 [intro]:
+ assumes "A \<in> null_sets N" "B \<in> sets M"
+ shows "A \<times> B \<in> null_sets (N \<Otimes>\<^sub>M M)"
+ using assms by (simp add: null_sets_def emeasure_pair_measure_Times)
+
+lemma (in sigma_finite_measure) times_in_null_sets2 [intro]:
+ assumes "A \<in> sets N" "B \<in> null_sets M"
+ shows "A \<times> B \<in> null_sets (N \<Otimes>\<^sub>M M)"
+ using assms by (simp add: null_sets_def emeasure_pair_measure_Times)
+
subsection \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
locale\<^marker>\<open>tag unimportant\<close> pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2