From b324dd7d84c73d42fc93d324098dc86021b34ad5 Mon Sep 17 00:00:00 2001
From: amethyst <yosukeito@itouyouukenoAir.lan>
Date: Sun, 11 Aug 2024 13:11:47 +0900
Subject: [PATCH 1/3] Add-Lemma_not_near_ninftyP

---
 CHANGELOG_UNRELEASED.md |  2 ++
 theories/normedtype.v   | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 698794d56..414e498f5 100644
--- 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
index 98739bc33..a067e9453 100644
--- 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

From e2f3e0b1c1f36439e1158ee70909d1abaa8d273e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 11 Aug 2024 21:02:12 +0900
Subject: [PATCH 2/3] trying to exploit symmetry (tentative)

---
 CHANGELOG_UNRELEASED.md |  6 +++++
 theories/normedtype.v   | 57 ++++++++++++++++++++++-------------------
 theories/topology.v     |  6 ++++-
 3 files changed, 42 insertions(+), 27 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 414e498f5..08e46fd4e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,12 @@
 - in `normedtype.v`:
   + lemmas `not_near_inftyP` `not_near_ninftyP`
 
+- in `topology.v`:
+  + lemma `filterN`
+
+- in `normedtype.v`:
+  + lemma `ninftyN`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/normedtype.v b/theories/normedtype.v
index a067e9453..d6b347cab 100644
--- a/theories/normedtype.v
+++ b/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.
@@ -432,18 +440,16 @@ 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.
+rewrite nearE -forallNP -propeqE; apply: eq_forall => M.
+by rewrite propeqE -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.
+rewrite -filterN ninftyN not_near_inftyP/=; split => Pf M; rewrite -realN;
+by move=> /Pf[x Mx Pfx]; exists (- x) => //; rewrite 1?(ltrNl,ltrNr,opprK).
 Qed.
 
 End infty_nbhs_instances.
@@ -1344,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.
@@ -1395,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 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; have := @not_near_at_rightP T (f \o -%R) (- p) P.
+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.
diff --git a/theories/topology.v b/theories/topology.v
index 1130813b3..7edf6f496 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -1423,6 +1423,11 @@ Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2).
 Ltac near_simpl := rewrite ?near_simpl.
 End NearMap.
 
+Lemma filterN {R : numDomainType} T (P : pred T) (f : R -> T) (F : set_system R) :
+  (\forall x \near - x @[x --> F], P ((f \o -%R) x)) =
+  \forall x \near F, P (f 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 +3455,6 @@ Qed.
 
 End set_nbhs.
 
-
 Section separated_topologicalType.
 Variable T : topologicalType.
 Implicit Types x y : T.

From f1a6057652c75e18c80489afa385c01bf5f7314c Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 11 Aug 2024 21:59:17 +0900
Subject: [PATCH 3/3] don't need to distinguish P and f?

---
 CHANGELOG_UNRELEASED.md |  5 ++++-
 theories/normedtype.v   | 34 +++++++++++++++++-----------------
 theories/topology.v     |  5 ++---
 3 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 08e46fd4e..9126cf21c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,7 +4,7 @@
 
 ### Added
 - in `normedtype.v`:
-  + lemmas `not_near_inftyP` `not_near_ninftyP`
+  + lemmas `not_near_inftyP`, `not_near_ninftyP`
 
 - in `topology.v`:
   + lemma `filterN`
@@ -14,6 +14,9 @@
 
 ### Changed
 
+- in `normedtype.v`:
+  + remove superflous parameters in lemmas `not_near_at_rightP` and `not_near_at_leftP`
+
 ### Renamed
 
 ### Generalized
diff --git a/theories/normedtype.v b/theories/normedtype.v
index d6b347cab..d4607ecf0 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -436,20 +436,20 @@ 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).
+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 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).
+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 => Pf M; rewrite -realN;
-by move=> /Pf[x Mx Pfx]; exists (- x) => //; rewrite 1?(ltrNl,ltrNr,opprK).
+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.
@@ -1381,21 +1381,21 @@ rewrite (@fun_predC _ -%R)/=; last exact: opprK.
 by rewrite image_id; under eq_fun do rewrite ltrNl opprK.
 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).
+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 pePf; apply: pPf; near=> t.
-apply: contrapT; apply: pePf; apply/andP; split.
+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 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).
+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 T (f \o -%R) (- p) P.
+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.
diff --git a/theories/topology.v b/theories/topology.v
index 7edf6f496..1303f173e 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -1423,9 +1423,8 @@ Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2).
 Ltac near_simpl := rewrite ?near_simpl.
 End NearMap.
 
-Lemma filterN {R : numDomainType} T (P : pred T) (f : R -> T) (F : set_system R) :
-  (\forall x \near - x @[x --> F], P ((f \o -%R) x)) =
-  \forall x \near F, P (f x).
+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}