equal
deleted
inserted
replaced
1755 apply auto |
1755 apply auto |
1756 done |
1756 done |
1757 |
1757 |
1758 lemma infinite_enumerate: |
1758 lemma infinite_enumerate: |
1759 assumes fS: "infinite S" |
1759 assumes fS: "infinite S" |
1760 shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)" |
1760 shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)" |
1761 unfolding subseq_def |
1761 unfolding strict_mono_def |
1762 using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto |
1762 using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto |
1763 |
1763 |
1764 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)" |
1764 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)" |
1765 apply auto |
1765 apply auto |
1766 apply (rule_tac x="d/2" in exI) |
1766 apply (rule_tac x="d/2" in exI) |