equal
deleted
inserted
replaced
596 lemma trans_inv_image: "trans r ==> trans (inv_image r f)" |
596 lemma trans_inv_image: "trans r ==> trans (inv_image r f)" |
597 apply (unfold trans_def inv_image_def) |
597 apply (unfold trans_def inv_image_def) |
598 apply (simp (no_asm)) |
598 apply (simp (no_asm)) |
599 apply blast |
599 apply blast |
600 done |
600 done |
|
601 |
|
602 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" |
|
603 by (auto simp:inv_image_def) |
601 |
604 |
602 |
605 |
603 subsection {* Finiteness *} |
606 subsection {* Finiteness *} |
604 |
607 |
605 lemma finite_converse [iff]: "finite (r^-1) = finite r" |
608 lemma finite_converse [iff]: "finite (r^-1) = finite r" |