author | krauss |
Mon, 26 Oct 2009 23:27:24 +0100 | |
changeset 33218 | ecb5cd453ef2 |
parent 33217 | ab979f6e99f4 |
child 33219 | a69147d95957 |
child 33234 | a5eba0447559 |
child 33250 | 5c2af18a3237 |
--- a/src/HOL/Relation.thy Mon Oct 26 23:27:16 2009 +0100 +++ b/src/HOL/Relation.thy Mon Oct 26 23:27:24 2009 +0100 @@ -607,6 +607,9 @@ lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" by (auto simp:inv_image_def) +lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f" +unfolding inv_image_def converse_def by auto + subsection {* Finiteness *}