| changeset 62101 | 26c0a70f78a3 |
| parent 61955 | e96292f32c3c |
| child 62139 | 519362f817c7 |
--- a/src/HOL/Product_Type.thy Fri Jan 08 16:37:56 2016 +0100 +++ b/src/HOL/Product_Type.thy Fri Jan 08 17:40:59 2016 +0100 @@ -1068,6 +1068,9 @@ lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))" by blast +lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B" + by (induct x) simp + lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})" by auto