equal
deleted
inserted
replaced
604 apply blast |
604 apply blast |
605 done |
605 done |
606 |
606 |
607 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" |
607 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" |
608 by (auto simp:inv_image_def) |
608 by (auto simp:inv_image_def) |
|
609 |
|
610 lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f" |
|
611 unfolding inv_image_def converse_def by auto |
609 |
612 |
610 |
613 |
611 subsection {* Finiteness *} |
614 subsection {* Finiteness *} |
612 |
615 |
613 lemma finite_converse [iff]: "finite (r^-1) = finite r" |
616 lemma finite_converse [iff]: "finite (r^-1) = finite r" |