--- a/src/HOL/Product_Type.thy Tue Mar 26 22:18:30 2019 +0100
+++ b/src/HOL/Product_Type.thy Wed Mar 27 14:08:26 2019 +0000
@@ -1272,6 +1272,17 @@
proc = K Set_Comprehension_Pointfree.code_simproc}])
\<close>
+subsection \<open>Lemmas about disjointness\<close>
+
+lemma disjnt_Times1_iff [simp]: "disjnt (C \<times> A) (C \<times> B) \<longleftrightarrow> C = {} \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Times2_iff [simp]: "disjnt (A \<times> C) (B \<times> C) \<longleftrightarrow> C = {} \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
+lemma disjnt_Sigma_iff: "disjnt (Sigma A C) (Sigma B C) \<longleftrightarrow> (\<forall>i \<in> A\<inter>B. C i = {}) \<or> disjnt A B"
+ by (auto simp: disjnt_def)
+
subsection \<open>Inductively defined sets\<close>