add in_nearW

IshiguroYoshihiro · Oct 1, 2024 · c87bccc · c87bccc
1 parent c963835
commit c87bccc
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git 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
@@ -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.