src/HOL/Library/FuncSet.thy
changeset 31769 d5f39775edd2
parent 31731 7ffc1a901eea
child 31770 ba52fcfaec28
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:31:27 2009 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:31:28 2009 +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 funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
     1.8 +  by (auto intro: Pi_I)
     1.9 +
    1.10  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
    1.11    by (simp add: Pi_def)
    1.12