equal
deleted
inserted
replaced
758 |
758 |
759 lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r" |
759 lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r" |
760 by (auto simp: total_on_def) |
760 by (auto simp: total_on_def) |
761 |
761 |
762 lemma finite_converse [iff]: "finite (r^-1) = finite r" |
762 lemma finite_converse [iff]: "finite (r^-1) = finite r" |
763 unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def) |
763 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] |
|
764 by (auto elim: finite_imageD simp: inj_on_def) |
764 |
765 |
765 lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>" |
766 lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>" |
766 by (auto simp add: fun_eq_iff) |
767 by (auto simp add: fun_eq_iff) |
767 |
768 |
768 lemma conversep_eq [simp]: "(op =)^--1 = op =" |
769 lemma conversep_eq [simp]: "(op =)^--1 = op =" |