# Zulip Chat Archive

## Stream: new members

### Topic: Proving a limit

#### Michał Mrugała (Sep 29 2022 at 13:55):

Hello everyone,

I'm having trouble finding the relevant lemmas in mathlib to prove the following limit:

```
example {c : ℝ} (hc : 0 < c) : filter.tendsto (λ n : ℕ, (1 + (n : ℝ)*c)^(1 / (n : ℝ))) filter.at_top (nhds 1) := sorry
```

I've previously proven:

```
example {N : ℝ} (hN : 0 < N) : filter.tendsto (λ n : ℕ, N ^ (1 / (n : ℝ))) filter.at_top (nhds 1) := sorry
```

Would anyone have an idea for how to deal with this?

#### Filippo A. E. Nuccio (Sep 29 2022 at 13:59):

Have you tried combining docs#filter.tendsto.const_add and docs#filter.tendsto.mul_const ?

#### Michał Mrugała (Sep 29 2022 at 14:03):

I can't see how these two lemmas would be helpful in this case, since addition and multiplication happens before introducing the exponent.

#### Filippo A. E. Nuccio (Sep 29 2022 at 14:11):

Ah, sorry, I have not seen you also had an exponent. Does docs#filter.tendsto.of_tendsto_comp help, together with the above two?

#### Michał Mrugała (Sep 29 2022 at 14:20):

I'd be surprised, since the expression we're applying the exponent to diverges.

#### Heather Macbeth (Sep 29 2022 at 14:26):

You can probably use docs#tendsto_rpow_div_mul_add composed with the continuity of a linear function and the nat-to-real coercion.

Last updated: Dec 20 2023 at 11:08 UTC