nat pow tendsto

Stream: Is there code for X?

[Jireh Loreaux]

Do we already have tendsto (λ n : ℕ, (2 : ℕ) ^ n) at_top at_top? Or with 2 replaced by any natural greater than one (I only need 2 though)? I checked specific_limits and only saw versions where the base was real, and I specifically need ℕ → ℕ.

[Jireh Loreaux]

I can prove it myself using tendsto_at_top_at_top_of_monotone, but I thought it might exist already.

[Yury G. Kudryashov]

docs#nat.tendsto_pow_at_top_at_top_of_one_lt