From 96d92cceba844579ea6ab379f2bfcbc5f86dc19e Mon Sep 17 00:00:00 2001
From: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
Date: Tue, 1 Oct 2024 10:58:03 +0900
Subject: [PATCH] add in_nearW

---
 CHANGELOG_UNRELEASED.md |  3 +++
 theories/topology.v     | 10 ++++++++++
 2 files changed, 13 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f938fac2e..b81edda14 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -16,6 +16,9 @@
 - in `realfun.v`:
   + lemmas `cvg_pinftyP`, `cvg_ninftyP`
 
+- in `topology.v`:
+  + lemma `in_nearW`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/topology.v b/theories/topology.v
index 123ab26ce..4eff4ff4f 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -7176,3 +7176,13 @@ Qed.
 Local Close Scope relation_scope.
 
 #[global] Hint Resolve uniform_regular : core.
+
+Lemma in_nearW (R : topologicalType) (P : R -> Prop) (S : set R) :
+  @open R^o S ->
+ {in S, forall x, P x} ->
+ {in S, forall x, \near x, P x}.
+Proof.
+move=> oS HP z /set_mem Sz.
+rewrite -nbhs_nearE nbhsE/=.
+by exists S; last move=> x /mem_set/HP.
+Qed.