Add lemmas not_near_inftyP and not_near_ninftyP in normedtype.v (…

…#1291)

* Add-Lemma_not_near_ninftyP

---------

Co-authored-by: amethyst <[email protected]>
Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,14 @@
 ## [Unreleased]
 
 ### Added
+- in `normedtype.v`:
+  + lemmas `not_near_inftyP`, `not_near_ninftyP`
+
+- in `topology.v`:
+  + lemma `filterN`
+
+- in `normedtype.v`:
+  + lemma `ninftyN`
 
 - in `derive.v`:
   + lemma `derive_id`
@@ -22,6 +30,9 @@
 
 ### Changed
 
+- in `normedtype.v`:
+  + remove superflous parameters in lemmas `not_near_at_rightP` and `not_near_at_leftP`
+
 ### Renamed
 
 - in `lebesgue_measure.v`:

theories/normedtype.v

@@ -358,6 +358,14 @@ Notation "-oo_ R" := (ninfty_nbhs R)
 Notation "+oo" := (pinfty_nbhs _) : ring_scope.
 Notation "-oo" := (ninfty_nbhs _) : ring_scope.
 
+Lemma ninftyN {R : numFieldType} : (- x : R)%R @[x --> -oo] = +oo.
+Proof.
+apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
+  exists (- M); rewrite realN; split => // x.
+  by rewrite ltrNl => /MA/=; rewrite opprK.
+by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNr => /MA.
+Qed.
+
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
 Implicit Types r : R.
@@ -428,6 +436,22 @@ 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 (P : pred R) :
+  ~ (\forall x \near +oo, P x) <->
+    forall M : R, M \is Num.real -> exists2 x, M < x & ~ P x.
+Proof.
+rewrite nearE -forallNP -propeqE; apply: eq_forall => M.
+by rewrite propeqE -implypN existsPNP.
+Qed.
+
+Lemma not_near_ninftyP (P : pred R):
+  ~ (\forall x \near -oo, P x) <->
+    forall M : R, M \is Num.real -> exists2 x, x < M & ~ P x.
+Proof.
+rewrite -filterN ninftyN not_near_inftyP/=; split => PN M; rewrite -realN;
+by move=> /PN[x Mx PNx]; exists (- x) => //; rewrite 1?(ltrNl,ltrNr,opprK).
+Qed.
+
 End infty_nbhs_instances.
 
 #[global] Hint Extern 0 (is_true (_ < ?x)) => match goal with
@@ -1326,26 +1350,6 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y.
 Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
 Unshelve. all: by end_near. Qed.
 
-Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) :
-  ~ (\forall x \near p^'+, P (f x)) ->
-  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x).
-Proof.
-move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
-apply: contrapT; apply: pePf; apply/andP; split.
-- by near: t; exact: nbhs_right_gt.
-- by near: t; apply: nbhs_right_lt; rewrite ltrDl.
-Unshelve. all: by end_near. Qed.
-
-Lemma not_near_at_leftP T (f : R -> T) (p : R) (P : pred T) :
-  ~ (\forall x \near p^'-, P (f x)) ->
-  forall e : {posnum R}, exists2 x : R, p - e%:num < x < p & ~ P (f x).
-Proof.
-move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
-apply: contrapT; apply: pePf; apply/andP; split.
-- by near: t; apply: nbhs_left_gt; rewrite ltrBlDr ltrDl.
-- by near: t; exact: nbhs_left_lt.
-Unshelve. all: by end_near. Qed.
-
 Lemma withinN (A : set R) a :
   within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)].
 Proof.
@@ -1377,6 +1381,25 @@ rewrite (@fun_predC _ -%R)/=; last exact: opprK.
 by rewrite image_id; under eq_fun do rewrite ltrNl opprK.
 Qed.
 
+Lemma not_near_at_rightP (p : R) (P : pred R) :
+  ~ (\forall x \near p^'+, P x) ->
+  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P x.
+Proof.
+move=> pPf e; apply: contrapT => /forallPNP peP; apply: pPf; near=> t.
+apply: contrapT; apply: peP; apply/andP; split.
+- by near: t; exact: nbhs_right_gt.
+- by near: t; apply: nbhs_right_lt; rewrite ltrDl.
+Unshelve. all: by end_near. Qed.
+
+Lemma not_near_at_leftP (p : R) (P : pred R) :
+  ~ (\forall x \near p^'-, P x) ->
+  forall e : {posnum R}, exists2 x : R, p - e%:num < x < p & ~ P x.
+Proof.
+move=> pPf e; have := @not_near_at_rightP (- p) (P \o -%R).
+rewrite at_rightN => /(_ _ e)[|x pxe Pfx]; first by rewrite filterN.
+by exists (- x) => //; rewrite ltrNl ltrNr opprB addrC andbC.
+Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.

theories/topology.v

@@ -1423,6 +1423,10 @@ Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2).
 Ltac near_simpl := rewrite ?near_simpl.
 End NearMap.
 
+Lemma filterN {R : numDomainType} (P : pred R) (F : set_system R) :
+  (\forall x \near - x @[x --> F], (P \o -%R) x) = \forall x \near F, P x.
+Proof. by rewrite near_simpl/= !nearE; under eq_fun do rewrite opprK. Qed.
+
 Lemma cvg_pair {T U V F} {G : set_system U} {H : set_system V}
   {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) :
   f @ F --> G -> g @ F --> H ->
@@ -3450,7 +3454,6 @@ Qed.
 
 End set_nbhs.
 
-
 Section separated_topologicalType.
 Variable T : topologicalType.
 Implicit Types x y : T.