equal
deleted
inserted
replaced
70 qed |
70 qed |
71 |
71 |
72 lemma countable_infiniteE': |
72 lemma countable_infiniteE': |
73 assumes "countable A" "infinite A" |
73 assumes "countable A" "infinite A" |
74 obtains g where "bij_betw g (UNIV :: nat set) A" |
74 obtains g where "bij_betw g (UNIV :: nat set) A" |
75 using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast |
75 by (meson assms bij_betw_inv countableE_infinite) |
76 |
76 |
77 lemma countable_enum_cases: |
77 lemma countable_enum_cases: |
78 assumes "countable S" |
78 assumes "countable S" |
79 obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}" |
79 obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}" |
80 | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV" |
80 | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV" |