lemmas regarding ε > 0

Stream: Is there code for X?

[Ashvni Narayanan]

I am looking for the following lemma :

lemma (ε : ℝ) (h : 0 < ε) : ∃ (n : ℕ), (1 / (p^n) : ℝ) < ε :=

Is there a place where lemmas of this kind are stored? Thank you!

[Kevin Buzzard]

I'm pretty sure that there's a lemma in mathlib saying there's N>0 such that 1/N < eps, so it now remains to prove that there's n such that p^n>=N. You don't say what p is in your file but given that you're a number theorist I'm betting that p is a prime :-) Do we have that 2^N > N? This is true for all N and it comes from Cantor's diagonal argument although of course the proof will not use this.

[Adam Topaz]

The best I could find is docs#archimedean

[Alex J. Best]

like docs#exists_pow_lt_of_lt_one is quite close?

[Damiano Testa]

Following Kevin's approach, there is also docs#nat.lt_two_pow.

[Adam Topaz]

And even docs#nat.lt_pow_self :wink:

[Ashvni Narayanan]

Alex J. Best said:

like docs#exists_pow_lt_of_lt_one is quite close?

This worked out. Thanks all!