Stream: math-comp analysis

Topic: A global property is also asymptotic

view this post on Zulip Julien Puydt (Nov 11 2022 at 09:54):

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).
by exists 0%N.

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.

Last updated: Feb 05 2023 at 13:02 UTC