| changeset 71848 | 3c7852327787 |
| parent 71827 | 5e315defb038 |
| child 71886 | 4f4695757980 |
--- a/src/HOL/Set.thy Wed May 20 08:33:53 2020 +0200 +++ b/src/HOL/Set.thy Wed May 20 15:00:25 2020 +0100 @@ -1246,6 +1246,9 @@ lemma disjoint_eq_subset_Compl: "A \<inter> B = {} \<longleftrightarrow> A \<subseteq> - B" by blast +lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x. x\<in>A \<longrightarrow> x \<notin> B)" + by blast + lemma disjoint_iff_not_equal: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)" by blast