src/HOL/Analysis/Linear_Algebra.thy
changeset 66447 a1f5c5c26fa6
parent 66420 bc0dab0e7b40
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -1757,8 +1757,8 @@
     1.4  
     1.5  lemma infinite_enumerate:
     1.6    assumes fS: "infinite S"
     1.7 -  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
     1.8 -  unfolding subseq_def
     1.9 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
    1.10 +  unfolding strict_mono_def
    1.11    using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
    1.12  
    1.13  lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"