Add-Lemma_not_near_ninftyP

math-comp · Aug 11, 2024 · b324dd7 · b324dd7
1 parent 99c3a83
commit b324dd7
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -3,6 +3,8 @@
 ## [Unreleased]
 
 ### Added
+- in `normedtype.v`:
+  + lemmas `not_near_inftyP` `not_near_ninftyP`
 
 ### Changed
 

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -428,6 +428,24 @@ move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM.
 by move=> x; rewrite -ltr_pdivlMr //; exact: AM.
 Qed.
 
+Lemma not_near_inftyP T (f : R -> T) (P : pred T):
+  ~ (\forall x \near +oo, P (f x)) <->
+    forall M : R, M \is Num.real -> exists2 x, M < x & ~ P (f x).
+Proof.
+rewrite nearE /ninfty_nbhs -forallNP.
+rewrite -propeqE; apply: eq_forall => M; rewrite propeqE.
+by rewrite -implypN existsPNP.
+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