I had to prove the following lemma during one of my experiments:

```
Section Missing.
Variable P: nat -> Prop.
Lemma asymptotic_because_everywhere:
(forall n, P n) -> (\forall n \near \oo, P n).
Proof.
by exists 0%N.
Qed.
End Missing.
```

It must already be there somewhere, but I didn't find under which name... what is it?

Notice that without this lemma, trying `exists 0%N => //`

in another of my proofs leads to a goal looking like this:

```
[set n | (0 <= n)%N]
`<=` (fun n : nat => P n)
```

which I found inacceptable: too complex!

With the above lemma, I can solve the same goal with:

```
apply: asymptotic_because_everywhere.
by apply: result_everywhere.
```

which is nice enough.

maybe nearW in topology.v

You're right, that's it!

Thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Jun 25 2024 at 18:02 UTC