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