src/HOL/Library/FuncSet.thy
changeset 47761 dfe747e72fa8
parent 44382 9afa4a0e6f3c
child 50104 de19856feb54
     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed Apr 25 17:15:10 2012 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed Apr 25 19:26:00 2012 +0200
     1.3 @@ -63,6 +63,9 @@
     1.4  lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
     1.5    by (simp add: Pi_def)
     1.6  
     1.7 +lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
     1.8 +  unfolding Pi_def by auto
     1.9 +
    1.10  lemma PiE [elim]:
    1.11    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
    1.12  by(auto simp: Pi_def)