Julien Puydt (Nov 11 2022 at 09:54): 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.
Reynald Affeldt (Nov 11 2022 at 11:38):maybe nearW in topology.v
Reynald Affeldt (Nov 11 2022 at 11:40): Julien Puydt (Nov 11 2022 at 11:48):You're right, that's it!
Thanks!
Notification Bot (Nov 11 2022 at 11:48):Julien Puydt has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC