src/HOL/Library/FuncSet.thy
changeset 38656 d5d342611edb
parent 33271 7be66dee1a5a
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Aug 23 17:46:13 2010 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Aug 23 19:35:57 2010 +0200
     1.3 @@ -67,6 +67,10 @@
     1.4    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     1.5  by(auto simp: Pi_def)
     1.6  
     1.7 +lemma Pi_cong:
     1.8 +  "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B"
     1.9 +  by (auto simp: Pi_def)
    1.10 +
    1.11  lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
    1.12    by (auto intro: Pi_I)
    1.13