equal
deleted
inserted
replaced
844 lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred] |
844 lemmas left_unique_rel_fset[transfer_rule] = left_unique_rel_set[Transfer.transferred] |
845 |
845 |
846 thm right_unique_rel_fset left_unique_rel_fset |
846 thm right_unique_rel_fset left_unique_rel_fset |
847 |
847 |
848 lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)" |
848 lemma bi_unique_rel_fset[transfer_rule]: "bi_unique A \<Longrightarrow> bi_unique (rel_fset A)" |
849 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff) |
849 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_alt_def) |
850 |
850 |
851 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)" |
851 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)" |
852 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff) |
852 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_alt_def) |
853 |
853 |
854 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred] |
854 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred] |
855 |
855 |
856 |
856 |
857 subsubsection {* Quotient theorem for the Lifting package *} |
857 subsubsection {* Quotient theorem for the Lifting package *} |