From 414060aab4c5bc9de56388a151be21a4889b2cff Mon Sep 17 00:00:00 2001 From: amethyst Date: Tue, 6 Aug 2024 20:54:52 +0900 Subject: [PATCH] Add-Lemma_not_near_ninftyP --- theories/normedtype.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/normedtype.v b/theories/normedtype.v index af25c6317..2a64288ab 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -428,6 +428,15 @@ move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM. by move=> x; rewrite -ltr_pdivlMr //; exact: AM. Qed. +Lemma not_near_ninftyP T (f : R -> T) (P : pred T): + ~ (\forall x \near -oo, P (f x)) <-> + forall M : R, M \is Num.real -> exists2 x, x < M & ~ P (f x). +Proof. +rewrite nearE /ninfty_nbhs -forallNP. +rewrite -propeqE; apply: eq_forall => M; rewrite propeqE. +by rewrite -implypN existsPNP. +Qed. + End infty_nbhs_instances. #[global] Hint Extern 0 (is_true (_ < ?x)) => match goal with