diff -r 5bbb2bd564fa -r 09bb8f470959 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Dec 27 22:54:29 2018 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Dec 27 23:38:55 2018 +0100
@@ -266,6 +266,12 @@
   finally show ?case by simp
 qed
 
+lemma infinite_enumerate:
+  assumes fS: "infinite S"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
+  unfolding strict_mono_def
+  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
+
 lemma enumerate_Suc'':
   fixes S :: "'a::wellorder set"
   assumes "infinite S"