lemma converse_inv_image
authorkrauss
Mon Oct 26 23:27:24 2009 +0100 (2009-10-26)
changeset 33218ecb5cd453ef2
parent 33217 ab979f6e99f4
child 33219 a69147d95957
child 33234 a5eba0447559
child 33250 5c2af18a3237
lemma converse_inv_image
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Mon Oct 26 23:27:16 2009 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Oct 26 23:27:24 2009 +0100
     1.3 @@ -607,6 +607,9 @@
     1.4  lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
     1.5    by (auto simp:inv_image_def)
     1.6  
     1.7 +lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
     1.8 +unfolding inv_image_def converse_def by auto
     1.9 +
    1.10  
    1.11  subsection {* Finiteness *}
    1.12