# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464094624 -3600
# Node ID 360d9997fac94439630d8a5d5c05b9df0f9f67aa
# Parent  2b50f79829d24bfbecc1dcbc9aaebb9ab8fa467d
new theorem

diff -r 2b50f79829d2 -r 360d9997fac9 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Mon May 23 16:03:29 2016 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue May 24 13:57:04 2016 +0100
@@ -105,6 +105,11 @@
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
 
+lemma countable_as_injective_image:
+  assumes "countable A" "infinite A"
+  obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
+by (metis bij_betw_def bij_betw_from_nat_into [OF assms])
+
 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
   by (cases "finite A") (auto simp: bij_betw_def)