From 15bd3e9f2620d0252a96eb87ecbdcd3d54f56480 Mon Sep 17 00:00:00 2001
From: IshYosh <103252572+IshiguroYoshihiro@users.noreply.github.com>
Date: Tue, 1 Oct 2024 12:53:44 +0900
Subject: [PATCH] add in_nearW (#1332)

* add in_nearW

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
---
 CHANGELOG_UNRELEASED.md |  3 +++
 theories/topology.v     | 19 ++++++++++++++++---
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f938fac2e..01206ab53 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -16,6 +16,9 @@
 - in `realfun.v`:
   + lemmas `cvg_pinftyP`, `cvg_ninftyP`
 
+- in `topology.v`:
+  + lemmas `in_nearW`, `open_in_nearW`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/topology.v b/theories/topology.v
index 123ab26ce..2c62a7556 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -782,6 +782,13 @@ Arguments filter_not_empty {T} F {_}.
 
 Notation ProperFilter := ProperFilter'.
 
+Lemma in_nearW {T : Type} (F : set_system T) (P : T -> Prop) (S : set T) :
+  Filter F -> F S -> {in S, forall x, P x} -> \near F, P F.
+Proof.
+move=> FF FS SP; rewrite -nbhs_nearE.
+by apply: (@filterS _ F _ S) => // x /mem_set /SP.
+Qed.
+
 Lemma filter_setT (T' : Type) : Filter [set: set T'].
 Proof. by constructor. Qed.
 
@@ -980,7 +987,7 @@ Arguments near {T F P} FP x Px.
 
 Lemma nearW {T : Type} {F : set_system T} (P : T -> Prop) :
   Filter F -> (forall x, P x) -> (\forall x \near F, P x).
-Proof. by move=> FF FP; apply: filterS filterT. Qed.
+Proof. by move=> FF FP; exact: (in_nearW _ filterT). Qed.
 
 Lemma filterE {T : Type} {F : set_system T} :
   Filter F -> forall P : set T, (forall x, P x) -> F P.
@@ -1799,16 +1806,22 @@ Qed.
 
 End Topological1.
 
+Lemma open_in_nearW {T : topologicalType} (P : T -> Prop) (S : set T) :
+  open S -> {in S, forall x, P x} -> {in S, forall x, \near x, P x}.
+Proof.
+by move=> oS SP z /set_mem Sz; apply: in_nearW SP => //=; exact: open_nbhs_nbhs.
+Qed.
+
 #[global] Hint Extern 0 (Filter (nbhs _)) =>
   solve [apply: nbhs_filter] : typeclass_instances.
 #[global] Hint Extern 0 (ProperFilter (nbhs _)) =>
   solve [apply: nbhs_pfilter] : typeclass_instances.
 
-Global Instance alias_nbhs_filter {T : topologicalType} x : 
+Global Instance alias_nbhs_filter {T : topologicalType} x :
   @Filter T^o (@nbhs T^o T x).
 Proof. apply: @nbhs_filter T x. Qed.
 
-Global Instance alias_nbhs_pfilter {T : topologicalType} x : 
+Global Instance alias_nbhs_pfilter {T : topologicalType} x :
   @ProperFilter T^o (@nbhs T^o T x).
 Proof. exact: @nbhs_pfilter T x. Qed.