equal
deleted
inserted
replaced
90 |
90 |
91 lemma rcset[simp]: |
91 lemma rcset[simp]: |
92 "countable (rcset C)" |
92 "countable (rcset C)" |
93 using Rep_cset by simp |
93 using Rep_cset by simp |
94 |
94 |
95 lemma rcset_inj[simp]: |
|
96 "rcset C = rcset D \<longleftrightarrow> C = D" |
|
97 by (metis acset_rcset) |
|
98 |
|
99 lemma rcset_surj: |
95 lemma rcset_surj: |
100 assumes "countable A" |
96 assumes "countable A" |
101 shows "\<exists> C. rcset C = A" |
97 shows "\<exists> C. rcset C = A" |
102 apply(cases rule: Rep_cset_cases[of A]) |
98 apply(cases rule: Rep_cset_cases[of A]) |
103 using assms by auto |
99 using assms by auto |