--- a/src/HOL/Library/Countable_Set.thy Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Library/Countable_Set.thy Thu Aug 30 17:20:54 2018 +0200
@@ -69,6 +69,11 @@
then show thesis ..
qed
+lemma countable_infiniteE':
+ assumes "countable A" "infinite A"
+ obtains g where "bij_betw g (UNIV :: nat set) A"
+ using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
+
lemma countable_enum_cases:
assumes "countable S"
obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"