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