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).
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.

view this post on Zulip Reynald Affeldt (Nov 11 2022 at 11:38):

maybe nearW in topology.v

view this post on Zulip Reynald Affeldt (Nov 11 2022 at 11:40):

https://github.com/math-comp/analysis/blob/22a7476d5abafe0d6177c540125ce8e5069a4a70/theories/topology.v#L975-L977

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

You're right, that's it!

Thanks!

view this post on Zulip Notification Bot (Nov 11 2022 at 11:48):

Julien Puydt has marked this topic as resolved.


Last updated: Jun 25 2024 at 18:02 UTC