228 by (metis countable_vimage top_greatest) |
228 by (metis countable_vimage top_greatest) |
229 |
229 |
230 lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}" |
230 lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}" |
231 by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) |
231 by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) |
232 |
232 |
|
233 lemma countable_Image: |
|
234 assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})" |
|
235 assumes "countable Y" |
|
236 shows "countable (X `` Y)" |
|
237 proof - |
|
238 have "countable (X `` (\<Union>y\<in>Y. {y}))" |
|
239 unfolding Image_UN by (intro countable_UN assms) |
|
240 then show ?thesis by simp |
|
241 qed |
|
242 |
|
243 lemma countable_relpow: |
|
244 fixes X :: "'a rel" |
|
245 assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)" |
|
246 assumes Y: "countable Y" |
|
247 shows "countable ((X ^^ i) `` Y)" |
|
248 using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X) |
|
249 |
|
250 lemma countable_rtrancl: |
|
251 "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)" |
|
252 unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow) |
|
253 |
233 lemma countable_lists[intro, simp]: |
254 lemma countable_lists[intro, simp]: |
234 assumes A: "countable A" shows "countable (lists A)" |
255 assumes A: "countable A" shows "countable (lists A)" |
235 proof - |
256 proof - |
236 have "countable (lists (range (from_nat_into A)))" |
257 have "countable (lists (range (from_nat_into A)))" |
237 by (auto simp: lists_image) |
258 by (auto simp: lists_image) |