equal
deleted
inserted
replaced
851 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff) |
851 by (auto intro: right_unique_rel_fset left_unique_rel_fset iff: bi_unique_iff) |
852 |
852 |
853 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)" |
853 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)" |
854 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff) |
854 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff) |
855 |
855 |
856 lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred] |
856 lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred] |
857 |
857 |
858 |
858 |
859 subsubsection {* Quotient theorem for the Lifting package *} |
859 subsubsection {* Quotient theorem for the Lifting package *} |
860 |
860 |
861 lemma Quotient_fset_map[quot_map]: |
861 lemma Quotient_fset_map[quot_map]: |