| changeset 50104 | de19856feb54 |
| parent 47761 | dfe747e72fa8 |
| child 50123 | 69b35a75caf3 |
--- a/src/HOL/Library/FuncSet.thy Fri Nov 16 18:49:46 2012 +0100 +++ b/src/HOL/Library/FuncSet.thy Fri Nov 16 18:45:57 2012 +0100 @@ -81,7 +81,10 @@ by (simp add: Pi_def) lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B" -by auto + by auto + +lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B" + by auto lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})" apply (simp add: Pi_def, auto)