diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6e2cb2a576..eaac014e84 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -84,6 +84,9 @@
 - in `Rstruct_topology.v`:
   + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE`
 
+- in `topology_structure.v`:
+  + lemma `denseNE` now uses `exists2`
+
 ### Renamed
 
 - in `esum.v`:
@@ -108,6 +111,25 @@
   + `summable_integral_dirac` -> `esummable_integral_dirac`
 - `mathcomp_extra.v` -> `mathcomp_compat.v`
 
+- in `topology_structure.v`:
+  + `open_nbhs` -> `mem_open`
+  + `open_nbhsE` -> `mem_openE`
+  + `open_nbhsT` -> `mem_openT`
+  + `open_nbhsI` -> `mem_openI`
+  + `open_nbhs_nbhs` -> `mem_open_nbhs`
+
+- in `uniform_structure.v`:
+  + `open_nbhs_entourage` -> `mem_open_entourage`
+
+- in `pseudometric_structure.v`:
+  + `open_nbhs_ball` -> `mem_open_ball`
+
+- in `pseudo_metric_normed_Zmodule.v`:
+  + `ball_open_nbhs` -> `ball_mem_open`
+
+- in `normed_module.v`:
+  + `open_nbhs_closed_ball` -> `mem_open_closed_ball`
+
 ### Generalized
 
 - in `esum.v`:
@@ -168,6 +190,9 @@
     `setringDI`, `preimage_classes`, `preimage_classes_comp`
     (deprecated since 1.9.0)
 
+- in `uniform_structure.v`:
+  + notation `complete_ax` (was deprecated)
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/ftc.v b/theories/ftc.v
index cf889b51d5..536ebeacc7 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -285,7 +285,7 @@ Proof.
 move=> xu fi + fx.
 move: a fi => [b a fi /[1!(@lte_fin R)] ax|[|//] fi _].
 - near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)) => //.
-  + exact: ball_open_nbhs.
+  + exact: ball_mem_open.
   + exact: measurable_ball.
   + apply: measurable_funS fi => //; rewrite ball_itv.
     apply: (@subset_trans _ `](x - e)%R, u]) => //.
@@ -294,7 +294,7 @@ move: a fi => [b a fi /[1!(@lte_fin R)] ax|[|//] fi _].
     apply: subset_itvr; rewrite bnd_simp lerBrDr -lerBrDl.
     by near: e; apply: nbhs_right_ltW; rewrite subr_gt0.
 - near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)) => //.
-  + exact: ball_open_nbhs.
+  + exact: ball_mem_open.
   + exact: measurable_ball.
   + apply: measurable_funS fi => //; rewrite ball_itv.
     apply: (@subset_trans _ `](x - e)%R, u]) => //.
diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v
index 21cf3099b8..0e7f07d8e8 100644
--- a/theories/homotopy_theory/wedge_sigT.v
+++ b/theories/homotopy_theory/wedge_sigT.v
@@ -140,7 +140,7 @@ Proof.
 rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl.
   case=> V [/= oV Vp] VU j _; apply: wedge_lift_continuous.
   apply: (filterS VU); first exact: (@nbhs_filter wedge).
-  apply: open_nbhs_nbhs; split => //.
+  apply: mem_open_nbhs; split => //.
   by rewrite (wedge_liftE (p0 i0)).
 move=> Uj; have V_ : forall i, {V : set (X i) |
     [/\ open V, V (p0 i) & V `<=` @wedge_lift i @^-1` U]}.
@@ -303,7 +303,7 @@ exists (proj i @^-1` (@wedge_lift i @^-1`
   apply/ proj_continuous; rewrite /proj dfwith_in preimage_setI; apply: filterI.
     exact: wNz.
   have /filterS := @preimage_image _ _ (@wedge_lift i) (~` [set p0 i]).
-  by apply; apply: open_nbhs_nbhs; split; [exact: closed_openC|exact/eqP].
+  by apply; apply: mem_open_nbhs; split; [exact: closed_openC|exact/eqP].
 rewrite eqEsubset; split => // prodX; case => /[swap] [][] r _ <- /=.
   case => _ /[swap] /wedge_prod_inj -> [+ [e /[swap]]] => /[swap].
   move=> <- Awe eNpi; rewrite /proj /wedge_prod /=.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
index 725a47558a..e0ea8bf286 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -665,7 +665,7 @@ Unshelve. all: by end_near. Qed.
 
 Section continuous_cvg_davg.
 Context f (x : R) (U : set R).
-Hypotheses (xU : open_nbhs x U) (mU : measurable U) (mUf : measurable_fun U f)
+Hypotheses (xU : mem_open x U) (mU : measurable U) (mUf : measurable_fun U f)
            (fx : {for x, continuous f}).
 
 Let continuous_integralB_fin_num :
@@ -746,7 +746,7 @@ Proof. by apply: limf_esup_ge0 => // => y; exact: iavg_ge0. Qed.
 
 Import MeasurableR.
 
-Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U ->
+Lemma lim_sup_davg_le f g x (U : set R) : mem_open x U -> measurable U ->
   measurable_fun U f -> measurable_fun U g ->
   (f \+ g)%R^* x <= (f^* \+ g^*) x.
 Proof.
@@ -762,7 +762,7 @@ apply: measurable_funS mg => //; apply: exU => //=.
 by rewrite (lt_le_trans ry)//; near: r; exact: nbhs_right_le.
 Unshelve. all: by end_near. Qed.
 
-Lemma continuous_lim_sup_davg f x (U : set R) : open_nbhs x U -> measurable U ->
+Lemma continuous_lim_sup_davg f x (U : set R) : mem_open x U -> measurable U ->
   measurable_fun U f -> {for x, continuous f} ->
   f^* x = 0.
 Proof.
@@ -770,7 +770,7 @@ move=> xU mU mUf ctsf.
 by have /lim_lime_sup := continuous_cvg_davg xU mU mUf ctsf.
 Qed.
 
-Lemma lim_sup_davgB f g x (U : set R) : open_nbhs x U -> measurable U ->
+Lemma lim_sup_davgB f g x (U : set R) : mem_open x U -> measurable U ->
   measurable_fun U f -> {for x, continuous g} ->
   locally_integrable [set: R] g -> (f \- g)%R^* x = f^* x.
 Proof.
@@ -851,7 +851,7 @@ Definition lebesgue_pt {R : realType} (f : R -> R) (x : R) :=
 Import MeasurableR.
 
 Lemma continuous_lebesgue_pt {R : realType} (f : R -> R) x (U : set R) :
-  open_nbhs x U -> measurable U -> measurable_fun U f ->
+  mem_open x U -> measurable U -> measurable_fun U f ->
   {for x, continuous f} -> lebesgue_pt f x.
 Proof.
 move=> xU mU mUf xf; rewrite /lebesgue_pt -[X in _ --> X](@davg0 _ f x 0)//.
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index dd6f85b216..da73d76fbd 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -1590,7 +1590,7 @@ have mE k n : measurable (E k n).
 have nEcvg x k : exists n, A x -> (~` E k n) x.
   have [Ax|?] := pselect (A x); last by exists point.
   have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)).
-    by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
+    by apply: mem_open_nbhs; split; [exact: open_interior|exact: nbhsx_ballx].
   move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni.
   apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC.
   by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center.
@@ -1606,7 +1606,7 @@ have badn' k : exists n, mu (E k n) < ((eps / 2) / (2 ^ k.+1)%:R)%:E.
     - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []].
     - exact: bigcap_measurable.
   rewrite measure0; case/fine_cvg/(_ (interior (ball 0%R ek))).
-    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
+    apply/mem_open_nbhs/(mem_open_ball _ (@PosNum _ ek _)).
     by rewrite !divr_gt0.
   move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN.
   rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//.
diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index 89085de736..677b488e9d 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -71,8 +71,8 @@ exists (\row_j f j); split; first by move=> i; rewrite mxE; apply: Af.
 move=> C D FC f_D; have {}f_D :
   nbhs (f : prod_topology _) [set g | D (\row_j g j)].
   have [E f_E sED] := f_D; rewrite nbhsE.
-  set Pj := fun j Bj => open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
-  have exPj : forall j, exists Bj, open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
+  set Pj := fun j Bj => mem_open (f j) Bj /\ Bj `<=` E ord0 j.
+  have exPj : forall j, exists Bj, mem_open (f j) Bj /\ Bj `<=` E ord0 j.
     move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj].
     by rewrite row_simpl'; exists Bj.
   exists [set g | forall j, (get (Pj j)) (g j)]; last first.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index d8720f1c64..f8163031ec 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -175,7 +175,7 @@ HB.structure Definition NormedVector (K : numDomainType) :=
 (**md see also `Section standard_topology_pseudoMetricNormedZmod` in
   `pseudometric_normed_Zmodule.v` *)
 Section standard_topology_normedMod.
-Variable R : numFieldType.
+Context {R : numFieldType}.
 
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).
@@ -1564,7 +1564,7 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
     have ? : ~ closure (A true) z.
       by move: sepA; rewrite /separated => -[] _ /disjoints_subset; apply.
     have ? : open (~` closure (A true)) by exact/closed_openC/closed_closure.
-    exact/nbhsC_ball/open_nbhs_nbhs.
+    exact/nbhsC_ball/mem_open_nbhs.
   pose z1 : R := z + r%:num / 2; exists z1.
   have z1y : z1 <= y.
     rewrite leNgt; apply/negP => yz1.
@@ -2203,7 +2203,7 @@ Qed.
 Lemma open_subball {R : numFieldType} {M : normedModType R} (A : set M)
   (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
 Proof.
-move=> oA Ax; have /nbhsr0P/= : nbhs x A by exact/open_nbhs_nbhs.
+move=> oA Ax; have /nbhsr0P/= : nbhs x A by exact/mem_open_nbhs.
 apply: filterS => e xeA y exy; apply: xeA.
 by rewrite -ball_normE/= in exy; exact: ltW.
 Qed.
@@ -2317,12 +2317,14 @@ apply lt_le_trans; rewrite ltr_pMl; first by rewrite normr_gt0 subr_eq0 eq_sym.
 by rewrite ger0_norm // ltrDl normr_gt0; near: e; exists 1 => /=.
 Unshelve. all: by end_near. Qed.
 
-Lemma open_nbhs_closed_ball (R : realType) (V : normedModType R) (x : V)
-  (r : R) : 0 < r -> open_nbhs x (closed_ball x r)°.
+Lemma mem_open_closed_ball (R : realType) (V : normedModType R) (x : V)
+  (r : R) : 0 < r -> mem_open x (closed_ball x r)°.
 Proof.
 move=> r0; split; first exact: open_interior.
 by rewrite interior_closed_ballE //; exact: ballxx.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_open_closed_ball)]
+Notation open_nbhs_closed_ball := mem_open_closed_ball (only parsing).
 
 Lemma locally_compactR (R : realType) : locally_compact [set: R].
 Proof.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 6f22a01566..e4619976ff 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -218,7 +218,7 @@ move=> z; rewrite -ball_normE/= ltrBrDr.
 by apply: le_lt_trans; rewrite [in leRHS]addrC ler_distD.
 Qed.
 
-Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
+Lemma ball_mem_open (x : V) (r : K) : 0 < r -> mem_open x (ball x r).
 Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
 
 (**md Neighborhoods defined by the norm: *)
@@ -379,6 +379,9 @@ by rewrite (_ : _ \o _ = A \o f) // funeqE=> z; rewrite /= opprD addNKr addrNK.
 Qed.
 
 End pseudoMetricNormedZmod_numDomainType.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=ball_mem_open)]
+Notation ball_open_nbhs := ball_mem_open (only parsing).
+
 #[global] Hint Resolve normr_ge0 : core.
 Arguments cvgr_dist_lt {_ _ _ F FF}.
 Arguments cvgr_distC_lt {_ _ _ F FF}.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 79719f209c..206bc2ac5e 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -560,7 +560,7 @@ split; first by exists [set: E]; split; first exact: filter_nbhsT.
   move=> P Q; rewrite /entourage nbhsE /=.
   move=> [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]].
   exists (U `&` V); split => [|xy].
-    by exists (B `&` C); [exact: open_nbhsI|exact: setISS].
+    by exists (B `&` C); [exact: mem_openI|exact: setISS].
   by rewrite !in_setI => /andP[/Bxy-> /Cxy->].
 by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ].
 Qed.
@@ -588,7 +588,7 @@ have := @add_continuous (0, 0); rewrite /continuous_at/= addr0 => /(_ U U0)[]/=.
 move=> [W1 W2] []; rewrite nbhsE/= => [[U1 nU1 UW1] [U2 nU2 UW2]] Wadd.
 exists [set w | (W1 `&` W2) (w.1 - w.2)].
   exists (W1 `&` W2); split; last by [].
-  exists (U1 `&` U2); first exact: open_nbhsI.
+  exists (U1 `&` U2); first exact: mem_openI.
   by move=> t [U1t U2t]; split; [exact: UW1|exact: UW2].
 move => xy /= [z [H1 _] [_ H2]]; apply/set_mem/(Uxy xy)/mem_set.
 rewrite [_ - _](_ : _ = (xy.1 - z) + (z - xy.2)); first by rewrite addrA subrK.
diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v
index bc0e9a656d..dd43f472e5 100644
--- a/theories/normedtype_theory/urysohn.v
+++ b/theories/normedtype_theory/urysohn.v
@@ -152,7 +152,7 @@ Proof.
 move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E.
   rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xy | edist xy = +oo]%E).
     by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->.
-  by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open.
+  by apply: mem_open_nbhs; split => //; exact: edist_pinfty_open.
 rewrite -ltey -ge0_fin_numE// => efin.
 rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin.
   by have := edist_fin_open efin; apply: filter_app; near=> w.
@@ -471,7 +471,7 @@ Proof.
 case; case => L R [/= oL oR AL cLR <-].
 have [R' []] : exists R', [/\ open R', closure L `<=` R' & closure R' `<=` R].
   have := @normalT (closure L) (@closed_closure T L).
-  case/(_ R); first by move=> x /cLR ?; apply: open_nbhs_nbhs.
+  case/(_ R); first by move=> x /cLR ?; apply: mem_open_nbhs.
   move=> V /set_nbhsP [U] [? ? ? cVR]; exists U; split => //.
   by apply: (subset_trans _ cVR); exact: closureS.
 move=> oR' cLR' cR'R; exists (apxU (L, R')), (apxU (R', R)).
@@ -550,7 +550,7 @@ Lemma normal_uniform_separator (B : set T) :
   closed A -> closed B -> A `&` B = set0 -> uniform_separator A B.
 Proof.
 move=> clA clB AB0; have /(_ (~`B))[x Ax|] := normalT clA.
-  apply: open_nbhs_nbhs; split => //.
+  apply: mem_open_nbhs; split => //.
   - exact/closed_openC.
   - by move: x Ax; apply/ disjoints_subset.
 move=> V /set_nbhsP [U [oU AU UV]] cVcb.
@@ -569,12 +569,12 @@ move=> [[/= P Q] [/= oP oQ AP cPQ <-]]; rewrite /apxU /=.
 set M := [set y | _ \/ _].
 have [Qx|nQx] := pselect (Q x); first last.
   suff -> : M = ~` closure P.
-    apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure.
+    apply: mem_open_nbhs; split; first exact/closed_openC/closed_closure.
     by move/cPQ.
   rewrite eqEsubset /M; split => z; first by do 2!case.
   by move=> ?; right; split => // /cPQ.
 have [nPx|cPx] := pselect (closure P x).
-  suff -> : M = Q by apply: open_nbhs_nbhs; split.
+  suff -> : M = Q by apply: mem_open_nbhs; split.
   rewrite eqEsubset /M; split => z; first by do 2!case.
   by move=> ?; left; split.
 suff -> : M = setT by exact: filterT.
@@ -603,7 +603,7 @@ exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split.
 - rewrite -subset0 => -[a b [[/= Aa Bb]]].
   by rewrite (imsub1 fA0)// (imsub1 fB1)// /ball/= sub0r normrN normr1 ltxx.
 - move=> x U [V [[W oW <- /=]]] ? /filterS; apply.
-  by apply: ctsf; exact: open_nbhs_nbhs.
+  by apply: ctsf; exact: mem_open_nbhs.
 Qed.
 
 Section normalP.
@@ -710,7 +710,7 @@ Let completely_regular_nbhsE : @nbhs X X = nbhs_ (@entourage X').
 Proof.
 rewrite nbhs_entourageE; apply/funext => x; apply/seteqP; split; first last.
   apply/cvg_sup => -[f ctsf] U [/= _ [[V /= oV <- /= Vfx]]] /filterS.
-  by apply; exact/ctsf/open_nbhs_nbhs.
+  by apply; exact/ctsf/mem_open_nbhs.
 move=> U; wlog oU : U / @open X U.
   move=> WH; rewrite nbhsE => -[V [oV Vx /filterS]].
   apply; first exact: (@nbhs_filter X').
@@ -812,7 +812,7 @@ Lemma regular_openP {T : topologicalType} (x : T) :
 Proof.
 split.
   move=> + A clA nAx => /(_ (~` A)) [].
-    by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
+    by apply: mem_open_nbhs; split => //; exact: closed_openC.
   move=> U Ux /subsetC; rewrite setCK => AclU; exists U°.
   exists (~` closure U) ; split => //; first exact: open_interior.
     exact/closed_openC/closed_closure.
@@ -821,7 +821,7 @@ split.
 move=> + A Ax => /(_ (~` A°)) []; [|exact|].
   exact/open_closedC/open_interior.
 move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U.
-  exact/open_nbhs_nbhs.
+  exact/mem_open_nbhs.
 apply: (subset_trans (closureS UV)).
 move/open_closedC/closure_id : oV => <-.
 by apply: (subset_trans cAV); rewrite setCK; exact: interior_subset.
diff --git a/theories/sequences.v b/theories/sequences.v
index a60149df00..e7630e563a 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -3123,7 +3123,7 @@ move=> odF D Dy OpenD.
 have /(_ D Dy OpenD)[a0 DF0a0] : dense (F 0%N) := proj2 (odF 0%N).
 have {OpenD Dy} openIDF0 : open (D `&` F 0%N).
   by apply: openI => //; exact: (proj1 (odF 0%N)).
-have /open_nbhs_nbhs/nbhs_closedballP[r0 Ball_a0] : open_nbhs a0 (D `&` F 0%N).
+have /mem_open_nbhs/nbhs_closedballP[r0 Ball_a0] : mem_open a0 (D `&` F 0%N).
   by [].
 pose P (m : nat) (arn : U * {posnum K}) (arm : U * {posnum K}) :=
   closed_ball arm.1 (arm.2%:num) `<=` (closed_ball arn.1 arn.2%:num)° `&` F m
@@ -3133,12 +3133,12 @@ have Ar : forall na : nat * (U * {posnum K}), exists b : U * {posnum K},
   move=> [n [an rn]].
   have [ openFn denseFn] := odF n.+1.
   have [an1 B0Fn2an1] : exists x, ((closed_ball an rn%:num)° `&` F n.+1) x.
-    have [//|? ?] := @open_nbhs_closed_ball _ _ an rn%:num.
+    have [//|? ?] := @mem_open_closed_ball _ _ an rn%:num.
     by apply: denseFn => //; exists an.
   have openIB0Fn1 : open ((closed_ball an rn%:num)° `&` F n.+1).
     by apply/openI => //; exact/open_interior.
-  have /open_nbhs_nbhs/nbhs_closedballP[rn01 Ball_an1] :
-    open_nbhs an1 ((closed_ball an rn%:num)° `&` F n.+1) by [].
+  have /mem_open_nbhs/nbhs_closedballP[rn01 Ball_an1] :
+    mem_open an1 ((closed_ball an rn%:num)° `&` F n.+1) by [].
   have n31_gt0 : n.+3%:R^-1 > 0 :> K by [].
   have majr : minr (PosNum n31_gt0)%:num rn01%:num > 0 by [].
   exists (an1, PosNum majr); split.
@@ -3282,8 +3282,8 @@ have ContraBaire : exists i, not (dense (O i)).
 have [n [x0 [r H]] k] :
     exists n x (r : {posnum K}), (ball x r%:num) `<=` (~` (O n)).
   move: ContraBaire =>
-  [i /(denseNE) [ O0 [ [ x /open_nbhs_nbhs /nbhs_ballP [r r0 bxr]
-   /((@subsetI_eq0 _ (ball x r) O0 (O i) (O i)))]]]] /(_ bxr) bxrOi.
+  [i /denseNE[ O0 [ x /mem_open_nbhs /nbhs_ballP [r r0 bxr]
+   /((@subsetI_eq0 _ (ball x r) O0 (O i) (O i)))]]] /(_ bxr) bxrOi.
   by exists i, x, (PosNum r0); apply/disjoints_subset/bxrOi.
 exists ((n + n)%:R * k * 2 / r%:num)=> f Ff y Hx; move: (Propf f Ff) => [ _ linf].
 have [->|Zeroy] := eqVneq y 0.
diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v
index e8b8cffe4c..a3da204e3a 100644
--- a/theories/topology_theory/compact.v
+++ b/theories/topology_theory/compact.v
@@ -56,7 +56,7 @@ Definition cluster (F : set_system T) := [set p : T | F `#` nbhs p].
 Lemma cluster_nbhs t : cluster (nbhs t) t.
 Proof. by move=> A B /nbhs_singleton At /nbhs_singleton Bt; exists t. Qed.
 
-Lemma clusterEonbhs F : cluster F = [set p | F `#` open_nbhs p].
+Lemma clusterEonbhs F : cluster F = [set p | F `#` mem_open p].
 Proof. by under eq_fun do rewrite -meets_openr. Qed.
 
 Lemma clusterE F : cluster F = \bigcap_(A in F) (closure A).
@@ -412,8 +412,8 @@ move=> D [] oD cD /=; have cmpt : cover_compact D.
   by rewrite -compact_cover; exact: (subclosed_compact _ cmpT).
 have h (x : T) : exists V : set T, D x -> [/\ B V, nbhs x V & V `<=` D].
   have [Dx|] := pselect (D x); last by move=> ?; exists set0.
-  have [V [BV Vx VD]] := Bbase x D (open_nbhs_nbhs (conj oD Dx)).
-  exists V => _; split => //; apply: open_nbhs_nbhs; split => //.
+  have [V [BV Vx VD]] := Bbase x D (mem_open_nbhs (conj oD Dx)).
+  exists V => _; split => //; apply: mem_open_nbhs; split => //.
   exact: obase.
 pose h' := fun z => projT1 (cid (h z)).
 have [fs fsD DsubC] : finite_subset_cover D h' D.
diff --git a/theories/topology_theory/connected.v b/theories/topology_theory/connected.v
index 1d468a2e1a..54fc5f61cb 100644
--- a/theories/topology_theory/connected.v
+++ b/theories/topology_theory/connected.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra all_classical.
 From mathcomp Require Import topology_structure.
@@ -151,7 +151,7 @@ suff : A `<=` U.
   by apply: closedI => //; exact: closed_closure.
 rewrite -setIidPl; apply: ctdA.
 - move: U0; rewrite C1E => -[z [clAx C1z]]; have [] := clAx C1.
-    exact: open_nbhs_nbhs.
+    exact: mem_open_nbhs.
   by move=> w [Aw C1w]; exists w; rewrite setIA (setIidl (@subset_closure _ _)).
 - by exists C1 => //; rewrite C1E setIA (setIidl (@subset_closure _ _)).
 - by exists C2 => //; rewrite C2E setIA (setIidl (@subset_closure _ _)).
diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v
index 1b3cb281cf..c582211da3 100644
--- a/theories/topology_theory/discrete_topology.v
+++ b/theories/topology_theory/discrete_topology.v
@@ -207,7 +207,7 @@ exact/principal_filterP.
 Qed.
 
 Lemma discrete_set1 (x : X) : nbhs x [set x].
-Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed.
+Proof. by apply: mem_open_nbhs; split => //; exact: discrete_open. Qed.
 
 Lemma discrete_closed (A : set X) : closed A.
 Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed.
diff --git a/theories/topology_theory/function_spaces.v b/theories/topology_theory/function_spaces.v
index ec20892bb0..7915242b38 100644
--- a/theories/topology_theory/function_spaces.v
+++ b/theories/topology_theory/function_spaces.v
@@ -193,7 +193,7 @@ have [L Lsub /[dup] VL <-] := QfinP _ JV; rewrite preimage_bigcap.
 apply: filter_bigI => /= M /[dup] LM /Lsub /set_mem [] w _ [+] + /[dup] + <-.
 have [->|wnx] := eqVneq w i => N oN NM.
   apply: (@filterS _ _ _ N); first by move=> ? ?; rewrite /= dfwith_in.
-  apply: open_nbhs_nbhs; split => //; move: Vpz.
+  apply: mem_open_nbhs; split => //; move: Vpz.
   by rewrite -VL => /(_ _ LM); rewrite -NM /= dfwith_in.
 apply: nearW => y /=; move: Vpz.
 by rewrite -VL => /(_ _ LM); rewrite -NM /= ?dfwith_out // eq_sym.
@@ -400,7 +400,7 @@ apply: (@filterS _ _ _ (range join_product `&` B)).
   case=> K [oK KsubA] /KsubA.
   have -> : proj i (join_product w) = f_ i w by [].
   by move=> /exists2P/forallNP/(_ w)/not_andP [] // /contrapT.
-apply: open_nbhs_nbhs; split; last by rewrite -jxy.
+apply: mem_open_nbhs; split; last by rewrite -jxy.
 apply: openI; first exact: open_subspaceT.
 apply: open_subspaceW; apply: open_comp; last exact/closed_openC/closed_closure.
 by move=> + _; exact: proj_continuous.
@@ -1460,10 +1460,10 @@ Proof.
 move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE => -[O [oO Ofuv]] /filterS.
 apply; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB].
 have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z).
-  have [] := reg v (f u @^-1` O); first by apply: cfp; exact: open_nbhs_nbhs.
+  have [] := reg v (f u @^-1` O); first by apply: cfp; exact: mem_open_nbhs.
   by move=> R ? ?; exists R.
 exists (f @^-1` [set g | g @` (B `&` closure R) `<=` O], B `&` closure R).
-  split; [apply/cf/open_nbhs_nbhs; split | apply: filterI] => //.
+  split; [apply/cf/mem_open_nbhs; split | apply: filterI] => //.
   - apply: compact_open_open => //; apply: compact_closedI => //.
     exact: closed_closure.
   - by move=> ? [x [? + <-]]; apply: RO.
@@ -1500,15 +1500,15 @@ move=> _ v Mv; move: v Mv Ki; near: p.
 have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f @^-1` O)).
   move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv.
   have [[P Q] [Pu Qv] PQO] : nbhs (u, v) (f @^-1` O).
-    by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: fMO; exists v.
+    by apply: ctsf; apply: mem_open_nbhs; split => //; apply: fMO; exists v.
   exists (Q, P); [by []| move=> [b a [/= Qb Pa Mb]]].
-  by apply: ctsf; apply: open_nbhs_nbhs; split => //; exact: PQO.
+  by apply: ctsf; apply: mem_open_nbhs; split => //; exact: PQO.
 move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv.
 have [P' P'u cPO] := regU u _ umb.
 pose L := [set h | h @` ((K `&` closure P') `*` M) `<=` O].
 exists (setT, P' `*` L).
   split => //; [exact: filterT|]; exists (P', L) => //; split => //.
-  apply: open_nbhs_nbhs; split; first apply: compact_open_open => //.
+  apply: mem_open_nbhs; split; first apply: compact_open_open => //.
     apply: compact_setX => //; apply: compact_closedI => //.
     exact: closed_closure.
   by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton.
@@ -1545,9 +1545,9 @@ case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V -> W | g @` Q `<=` O].
 pose L := [set h : U -> V -> W | h @` (fst @` K `&` P) `<=` R].
 exists ((P `&` P') `*` Q, L); first split => /=.
 - exists (P `&` P', Q) => //; split => //=; apply: filterI => //.
-  apply: ctsf; apply: open_nbhs_nbhs; split => // _ [b Qb <-].
+  apply: ctsf; apply: mem_open_nbhs; split => // _ [b Qb <-].
   by apply: (PQfO (u, b)); split => //; exact: nbhs_singleton.
-- rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split.
+- rewrite nbhs_simpl /=; apply: mem_open_nbhs; split.
     apply: compact_open_open => //; apply: compact_closedI => //.
     apply: continuous_compact => //; apply: continuous_subspaceT => x.
     exact: cvg_fst.
diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v
index ae2716be76..45a427cef4 100644
--- a/theories/topology_theory/initial_topology.v
+++ b/theories/topology_theory/initial_topology.v
@@ -92,7 +92,7 @@ Lemma cvg_image (F : set_system S) (s : S) :
 Proof.
 move=> FF fsurj; split=> [cvFs|cvfFfs].
   move=> A /initial_continuous [B [Bop Bs sBAf]].
-  have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs.
+  have /cvFs FB : nbhs (s : W) B by apply: mem_open_nbhs.
   rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB.
   exact: image_preimage.
 move=> A /= [_ [[B Bop <-] Bfs sBfA]].
@@ -163,7 +163,7 @@ Qed.
 Let initial_ent_nbhs : nbhs = nbhs_ initial_ent.
 Proof.
 rewrite predeq2E => x V; split.
-  case=> [? [[B  ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs.
+  case=> [? [[B  ? <-] ? BsubV]]; have: nbhs (f x) B by apply: mem_open_nbhs.
   move=> /nbhsP [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W.
   by move=> ? ?; exact/BsubV/WsubB.
 case=> W [V' entV' V'subW] /filterS; apply.
@@ -262,5 +262,5 @@ Lemma continuous_comp_initial {Y : choiceType} {X Z : topologicalType}
   continuous (w \o f) -> continuous f.
 Proof.
 move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf.
-exact: open_nbhs_nbhs.
+exact: mem_open_nbhs.
 Qed.
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index f2512e688f..3a2d5c5596 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -31,7 +31,7 @@ HB.instance Definition _ (R : numDomainType) := hasNbhs.Build R^o
 
 Module TopologicalNumDomainType.
 Section TopologicalNumDomainType.
-Variable (R : numDomainType).
+Context {R : numDomainType}.
 
 Lemma nbhs_filter (p : R^o) : ProperFilter (nbhs p).
 Proof.
diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v
index fd27586d3b..f51de118d6 100644
--- a/theories/topology_theory/order_topology.v
+++ b/theories/topology_theory/order_topology.v
@@ -265,13 +265,13 @@ wlog xy : x y / (x < y)%O.
 move=> _ U /=; rewrite (min_l (ltW xy)) => Ux.
 have [[z xzy]|/forallNP/= xNy] := pselect (exists z, x < z < y)%O.
   exists (U `&` `]-oo, z[, `]z, +oo[%classic) => /=.
-    split; [apply: filterI =>//|]; apply: open_nbhs_nbhs.
+    split; [apply: filterI =>//|]; apply: mem_open_nbhs.
     - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy].
     - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy].
   case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => az zb.
   by rewrite min_l// (ltW (lt_trans az _)).
 exists (U `&` `]-oo, y[, `]x, +oo[%classic) => /=.
-  split; [apply: filterI => //|]; apply: open_nbhs_nbhs.
+  split; [apply: filterI => //|]; apply: mem_open_nbhs.
   - by split; [exact: lray_open|rewrite set_itvE].
   - by split; [exact: rray_open|rewrite set_itvE].
 case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => ay xb.
@@ -304,13 +304,13 @@ wlog xy : x y / (x < y)%O.
 move=> _ U /=; rewrite (max_r (ltW xy)) => Ux.
 have [[z xzy]|/forallNP /= xNy] := pselect (exists z, x < z < y)%O.
   exists (`]-oo, z[%classic, U `&` `]z, +oo[) => /=.
-    split; [|apply: filterI =>//]; apply: open_nbhs_nbhs.
+    split; [|apply: filterI =>//]; apply: mem_open_nbhs.
     - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy].
     - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy].
   case=> a b /= [] + []; rewrite !in_itv andbT /= => az Ub zb.
   by rewrite (max_r (ltW (lt_trans az _))).
 exists (`]-oo, y[%classic, U `&` `]x, +oo[) => /=.
-  split; [|apply: filterI => //]; apply: open_nbhs_nbhs.
+  split; [|apply: filterI => //]; apply: mem_open_nbhs.
   - by split; [exact: lray_open|rewrite set_itvE].
   - by split; [exact: rray_open|rewrite set_itvE].
 case=> a b /=; rewrite !in_itv /= andbT => [/=] [ay] [Ub] xb.
diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v
index e1711cfd44..7b76019d03 100644
--- a/theories/topology_theory/pseudometric_structure.v
+++ b/theories/topology_theory/pseudometric_structure.v
@@ -212,7 +212,7 @@ Proof. exact: ball_triangle_subproof. Qed.
 Lemma nbhsx_ballx x (eps : R) : 0 < eps -> nbhs x (ball x eps).
 Proof. by move=> e0; apply/nbhs_ballP; exists eps. Qed.
 
-Lemma open_nbhs_ball x (eps : {posnum R}) : open_nbhs x (ball x eps%:num)°.
+Lemma mem_open_ball x (eps : {posnum R}) : mem_open x (ball x eps%:num)°.
 Proof.
 split; first exact: open_interior.
 by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhsx_ballx.
@@ -267,6 +267,8 @@ Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y :
 Proof. by move/cvgi_ballP. Qed.
 
 End pseudoMetricType_numDomainType.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_open_ball)]
+Notation open_nbhs_ball := mem_open_ball (only parsing).
 
 #[global] Hint Resolve nbhsx_ballx : core.
 
diff --git a/theories/topology_theory/quotient_topology.v b/theories/topology_theory/quotient_topology.v
index ca77bc2042..60ef196ad0 100644
--- a/theories/topology_theory/quotient_topology.v
+++ b/theories/topology_theory/quotient_topology.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra all_classical.
 From mathcomp Require Import topology_structure.
diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v
index 60ff99a030..3c00251a06 100644
--- a/theories/topology_theory/separation_axioms.v
+++ b/theories/topology_theory/separation_axioms.v
@@ -82,7 +82,7 @@ Lemma set_nbhsP (B : set T) :
    set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]).
 Proof.
 split; first last.
-  by case=> V [? AV /filterS +] x /AV ?; apply; apply: open_nbhs_nbhs.
+  by case=> V [? AV /filterS +] x /AV ?; apply; apply: mem_open_nbhs.
 move=> snB; have Ux x : exists U, A x -> [/\ U x, open U & U `<=` B].
   have [/snB|?] := pselect (A x); last by exists point.
   by rewrite nbhsE => -[V [? ? ?]]; exists V.
@@ -119,7 +119,7 @@ Proof.
 move=> ? cptV nxV PF FV clFx1 U nbhsU; rewrite nbhs_simpl.
 wlog oU : U nbhsU / open U.
   rewrite /= nbhsE in nbhsU; case: nbhsU => O oO OsubU /(_ O) WH.
-  by apply: (filterS OsubU); apply: WH; [exact: open_nbhs_nbhs | by case: oO].
+  by apply: (filterS OsubU); apply: WH; [exact: mem_open_nbhs | by case: oO].
 have /compact_near_coveringP : compact (V `\` U).
   apply: (subclosed_compact _ cptV) => //.
   by apply: closedI; [exact: compact_closed | exact: open_closedC].
@@ -157,7 +157,7 @@ rewrite propeqE; split => [T_filterT2|T_openT2] x y.
   by exists (oA, oB); rewrite ?inE; split => //; apply: subsetI_eq0 AIB_eq0.
 apply: contraPP => /eqP /T_openT2[[/=A B]].
 rewrite !inE => - [xA yB] [Aopen Bopen /eqP AIB_eq0].
-move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)).
+move=> /(_ A B (mem_open_nbhs _) (mem_open_nbhs _)).
 by rewrite -set0P => /(_ _ _)/negP; apply.
 Qed.
 
@@ -208,10 +208,10 @@ rewrite /interior nbhsE/=.
 exists U => // x Ux /=.
 rewrite not_limit_pointE.
 have [xa|xneqa] := eqVneq x a.
-  exists U; rewrite xa; first exact: open_nbhs_nbhs.
+  exists U; rewrite xa; first exact: mem_open_nbhs.
   by apply: subset_trans XAa; exact: setIS.
 exists (U `&` [set~ a]).
-  apply: open_nbhs_nbhs; split.
+  apply: mem_open_nbhs; split.
     apply: openI; first by case: oaU.
     by rewrite openC; exact: accessible_closed_set1.
   by split => //; exact/eqP.
@@ -258,7 +258,7 @@ move=> npzq; exists (`]-oo, q[, `]p, +oo[)%classic; split => //=.
 Qed.
 
 Section ball_hausdorff.
-Variables (R : numDomainType) (T : pseudoMetricType R).
+Context {R : numDomainType} {T : pseudoMetricType R}.
 
 Lemma ball_hausdorff : hausdorff_space T =
   forall (a b : T), a != b ->
@@ -267,8 +267,8 @@ Lemma ball_hausdorff : hausdorff_space T =
 Proof.
 rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
   move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]].
-  have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by apply: open_nbhs_nbhs.
-  have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by apply: open_nbhs_nbhs.
+  have /nbhs_ballP[_/posnumP[r] rA]: nbhs a A by exact: mem_open_nbhs.
+  have /nbhs_ballP[_/posnumP[s] rB]: nbhs b B by exact: mem_open_nbhs.
   by exists (r, s) => /=; rewrite (subsetI_eq0 _ _ ABeq0).
 move=> r s /eqP brs_eq0; exists ((ball a r%:num)°, (ball b s%:num)°) => /=.
   split; by rewrite inE; apply: nbhs_singleton; apply: nbhs_interior;
@@ -305,22 +305,22 @@ move=> lcpt hsdfX [x|] [y|] //=.
 Qed.
 
 Section hausdorff_topologicalType.
-Variable T : topologicalType.
+Context {T : topologicalType}.
 Implicit Types x y : T.
 
 Local Open Scope classical_set_scope.
-Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.
+Definition close x y : Prop := forall M, mem_open y M -> closure M x.
 
 Lemma closeEnbhs x : close x = cluster (nbhs x).
 Proof.
-transitivity (cluster (open_nbhs x)); last first.
+transitivity (cluster (mem_open x)); last first.
   by rewrite /cluster; under eq_fun do rewrite -meets_openl.
 rewrite clusterEonbhs /close funeqE => y /=; rewrite meetsC /meets.
 apply/eq_forall => A; rewrite forall_swap.
 by rewrite closureEonbhs/= meets_globallyl.
 Qed.
 
-Lemma closeEonbhs x : close x = [set y | open_nbhs x `#` open_nbhs y].
+Lemma closeEonbhs x : close x = [set y | mem_open x `#` mem_open y].
 Proof.
 by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
 Qed.
@@ -460,9 +460,9 @@ Lemma ball_close {R : numFieldType} {M : pseudoMetricType R} (x y : M) :
   close x y = forall eps : {posnum R}, ball x eps%:num y.
 Proof.
 rewrite propeqE; split => [cxy eps|cxy].
-  have := [elaborate cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos)].
+  have := [elaborate cxy _ (mem_open_ball _ (eps%:num/2)%:pos)].
   rewrite closureEonbhs/= meetsC meets_globallyr.
-  move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]].
+  move/(_ _ (mem_open_ball _ (eps%:num / 2)%:pos)) => [z [zx zy]].
   by apply: (@ball_splitl _ _ z); apply: interior_subset.
 rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]]
   /nbhs_ballP[_/posnumP[e1 e1A]].
@@ -495,8 +495,8 @@ rewrite eqEsubset; split; first last.
 move=> y /=; apply: contraPeq; move: sep; rewrite open_hausdorff => /[apply].
 move=> [[B A]]/=; rewrite ?inE; case=> By Ax [oB oA BA0].
 apply/existsNP; exists (closure A); apply/existsNP; exists B; apply/not_implyP.
-split; first by exists A => //; exact: open_nbhs_nbhs.
-apply/not_implyP; split; first exact: open_nbhs_nbhs.
+split; first by exists A => //; exact: mem_open_nbhs.
+apply/not_implyP; split; first exact: mem_open_nbhs.
 apply/set0P/negP; rewrite negbK; apply/eqP/disjoints_subset.
 have /closure_id -> : closed (~` B); first by exact: open_closedC.
 by apply/closureS/disjoints_subset; rewrite setIC.
@@ -526,7 +526,7 @@ have cvP (x : T) : A x -> \forall x' \near x & i \near F, (~` i) x'.
   have snBD : filter_from (set_nbhs (~` B)) closure (closure (~` closure D)).
     exists (closure (~` closure D)) => [z|].
       move=> nBZ; apply: filterS; first exact: subset_closure.
-      apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure.
+      apply: mem_open_nbhs; split; first exact/closed_openC/closed_closure.
       exact/(subsetC _ nBZ)/(subset_trans cDC).
     by have := @closed_closure _ (~` closure D); rewrite closure_id => <-.
   near=> y U => /=; have Dy : D° y by exact: (near nD _).
@@ -617,7 +617,7 @@ move=> /(_ _ _ setC (powerset_filter_from_filter PF))[].
   move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y.
     by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton.
   exists (~` C, [set U | U `<=` C]); first split.
-  - by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
+  - by apply: mem_open_nbhs; split => //; exact: closed_openC.
   - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans.
     by exists C => //; exists C.
   - by case=> i j [? /subsetC]; apply.
@@ -1110,7 +1110,7 @@ Lemma perfectTP {T} : perfect_set [set: T] <-> forall x : T, ~ open [set x].
 Proof.
 split.
   case=> _; rewrite eqEsubset; case=> _ + x Ox => /(_ x I [set x]).
-  by case; [by apply: open_nbhs_nbhs; split |] => y [+ _] => /[swap] -> /eqP.
+  by case; [by apply: mem_open_nbhs; split |] => y [+ _] => /[swap] -> /eqP.
 move=> NOx; split; [exact: closedT |]; rewrite eqEsubset; split => x // _.
 move=> U; rewrite nbhsE; case=> V [] oV Vx VU.
 have Vnx: V != [set x] by apply/eqP => M; apply: (NOx x); rewrite -M.
diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v
index 61ab361868..06bbc306e7 100644
--- a/theories/topology_theory/sigT_topology.v
+++ b/theories/topology_theory/sigT_topology.v
@@ -42,7 +42,7 @@ Local Lemma sigT_nbhs_nbhs x A: sigT_nbhs x A -> sigT_nbhs x (sigT_nbhs^~ A).
 Proof.
 case: x => i Xi /=.
 rewrite sigT_nbhsE /= nbhsE /= => -[W [oW Wz WlA]].
-by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs.
+by exists W => // x /= Wx; exact/(filterS WlA)/mem_open_nbhs.
 Qed.
 
 HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i}
@@ -68,7 +68,7 @@ Lemma sigT_openP (U : set {i & X i}) :
 Proof.
 split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous.
 rewrite openE => -[i x Uxi].
-by rewrite /interior /nbhs/= sigT_nbhsE; exact: open_nbhs_nbhs.
+by rewrite /interior /nbhs/= sigT_nbhsE; exact: mem_open_nbhs.
 Qed.
 
 Lemma sigT_continuous {Z : topologicalType} (f : forall i, X i -> Z) :
diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index 9fab8d53bc..1b70035d71 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -192,11 +192,11 @@ split; first last.
   by move: oV; rewrite openE /interior; exact.
 rewrite -open_subspaceIT => oUA.
 have oxF (x : T) : (U `&` A) x ->
-    exists2 V, open_nbhs (x : T) V & V `&` A `<=` U `&` A.
+    exists2 V, mem_open (x : T) V & V `&` A `<=` U `&` A.
   move=> /[dup] UAx /= [Ux Ax].
   have := oUA _ UAx; case: nbhs_subspaceP => // _.
   rewrite withinE /= => -[V nbhsV]; rewrite -setIA setIid => UV.
-  exists V°; first rewrite open_nbhsE; first split => //.
+  exists V°; first rewrite mem_openE; first split => //.
   - exact: open_interior.
   - exact: nbhs_interior.
   - by rewrite UV => t [/interior_subset].
@@ -204,7 +204,7 @@ pose f (x : T) :=
   if pselect ((U `&` A) x) is left e then projT1 (cid2 (oxF x e)) else set0.
 set V := \bigcup_(x in U `&` A) f x; exists V.
   apply: bigcup_open => i UAi; rewrite /f; case: pselect => // ?; case: cid2.
-  by move=> //= W; rewrite open_nbhsE => -[].
+  by move=> //= W; rewrite mem_openE => -[].
 rewrite eqEsubset /V /f; split.
   move=> t [[u]] UAu /=; case: pselect => //= ?.
   by case: cid2 => //= W _ + ? ? ; apply; exact.
diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v
index 0cf35ba159..46a7d3de74 100644
--- a/theories/topology_theory/supremum_topology.v
+++ b/theories/topology_theory/supremum_topology.v
@@ -166,7 +166,7 @@ exists (\bigcap_(w in [set` F]) f w); repeat split.
     move=> /= ? /imfsetP [[[/= i w /[dup] /asboolP entw ? Fiw ->]]].
     by apply/mem_set; rewrite /f /=; exists i => //; exact: open_interior.
   by rewrite set_imfset bigcap_image //=.
-- by IEntP=> ? ? /open_nbhs_entourage entw ??; apply entw.
+- by IEntP=> ? ? /entourage_mem_open entw ? ?; apply entw.
 - move=> t /= Ifwt.
   by apply/mem_set/FsubE => it /Ifwt/interior_subset => /set_mem.
 Qed.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index ca3115f5ec..3af50dcf43 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -6,10 +6,13 @@ From mathcomp Require Export filter.
 
 (**md**************************************************************************)
 (* # Basic topological notions                                                *)
+(*                                                                            *)
 (* This file develops tools for the manipulation of basic topological         *)
 (* notions. The development of topological notions builds on "filtered types" *)
 (* by extending the hierarchy.                                                *)
 (*                                                                            *)
+(* In the identifiers, "nbhs" is an abbreviation for "neighborhoods".         *)
+(*                                                                            *)
 (* ## Mathematical structures                                                 *)
 (* ### Topology                                                               *)
 (* ```                                                                        *)
@@ -23,7 +26,9 @@ From mathcomp Require Export filter.
 (*                     open == set of open sets                               *)
 (*                   closed == set of closed sets                             *)
 (*                 clopen U == U is both open and closed                      *)
-(*              open_nbhs p == set of open neighbourhoods of p                *)
+(*               mem_open p == the set of sets that are open and contain p    *)
+(*                             This is intended to represent the set of open  *)
+(*                             neighborhoods of p                             *)
 (*                  basis B == a family of open sets that converges to        *)
 (*                             each point                                     *)
 (*       second_countable T == T has a countable basis                        *)
@@ -120,7 +125,7 @@ HB.structure Definition SubTopological (V : topologicalType)
 Section Topological1.
 Context {T : topologicalType}.
 
-Definition open_nbhs (p : T) (A : set T) := open A /\ A p.
+Definition mem_open (p : T) (A : set T) := open A /\ A p.
 
 Definition basis (B : set_system T) :=
   B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x.
@@ -136,14 +141,14 @@ Proof. exact: (@nbhs_pfilter). Qed.
 Canonical nbhs_filter_on (x : T) := FilterType (nbhs x) (@nbhs_filter x).
 
 Lemma nbhsE (p : T) :
-  nbhs p = [set A : set T | exists2 B : set T, open_nbhs p B & B `<=` A].
+  nbhs p = [set A : set T | exists2 B : set T, mem_open p B & B `<=` A].
 Proof.
 have -> : nbhs p = [set A : set T | exists B, [/\ open B, B p & B `<=` A] ].
   exact: nbhsE_subproof.
 by rewrite predeqE => A; split=> [[B [?]]|[B[]]]; exists B.
 Qed.
 
-Lemma open_nbhsE (p : T) (A : set T) : open_nbhs p A = (open A /\ nbhs p A).
+Lemma mem_openE (p : T) (A : set T) : mem_open p A = (open A /\ nbhs p A).
 Proof.
 by rewrite nbhsE propeqE; split=> [[? ?]|[? [B [? ?] BA]]]; split => //;
   [exists A | exact: BA].
@@ -166,7 +171,7 @@ Proof. by rewrite nbhsE => - [? [_ ?]]; apply. Qed.
 
 Lemma nbhs_interior (p : T) (A : set T) : nbhs p A -> nbhs p A°.
 Proof.
-rewrite nbhsE /open_nbhs openE => - [B [Bop Bp] sBA].
+rewrite nbhsE /mem_open openE => - [B [Bop Bp] sBA].
 by exists B => // q Bq; apply: filterS sBA _; apply: Bop.
 Qed.
 
@@ -214,29 +219,39 @@ move=> p [i Di]; rewrite /interior nbhsE => - [B [Bop Bp] sBfi].
 by exists B => // ? /sBfi; exists i.
 Qed.
 
-Lemma open_nbhsT (p : T) : open_nbhs p setT.
-Proof. by split=> //; apply: openT. Qed.
+Lemma mem_openT (p : T) : mem_open p setT.
+Proof. by split=> //; exact: openT. Qed.
 
-Lemma open_nbhsI (p : T) : setI_closed (open_nbhs p).
+Lemma mem_openI (p : T) : setI_closed (mem_open p).
 Proof. by move=> A B [Aop Ap] [Bop Bp]; split => //; exact: openI. Qed.
 
-Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A.
-Proof. by rewrite nbhsE => p_A; exists A. Qed.
+Lemma mem_open_nbhs (p : T) : mem_open p `<=` nbhs p.
+Proof. by move=> A; rewrite nbhsE => p_A; exists A. Qed.
 
 Lemma interiorI (A B : set T) : (A `&` B)° = A° `&` B°.
 Proof.
 rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []].
 - by rewrite subsetI => // -[? ?]; split; exists B0.
 - by move=> -[B0 ? ?] [B1 ? ?]; exists (B0 `&` B1);
-  [exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]].
+  [exact: mem_openI | rewrite subsetI; split; apply: subIset; [left|right]].
 Qed.
 
 End Topological1.
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_open)]
+Notation open_nbhs := mem_open (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_openE)]
+Notation open_nbhsE := mem_openE (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_openT)]
+Notation open_nbhsT := mem_openT (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_openI)]
+Notation open_nbhsI := mem_openI (only parsing).
+#[deprecated(since="mathcomp-analysis 1.18.0", use=mem_open_nbhs)]
+Notation open_nbhs_nbhs := mem_open_nbhs (only parsing).
 
 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.
+by move=> oS SP z /set_mem Sz; apply: in_nearW SP => //=; exact: mem_open_nbhs.
 Qed.
 
 #[global] Hint Extern 0 (Filter (nbhs _)) =>
@@ -327,7 +342,7 @@ Proof.
 move=> frh hfrl X; rewrite nbhsE => -[Y [oY Yl]].
 move/filterS; apply; apply: frh.
 rewrite nbhsE; exists Y => //; split => //.
-have /hfrl : nbhs l Y by exact: open_nbhs_nbhs.
+have /hfrl : nbhs l Y by exact: mem_open_nbhs.
 by rewrite nbhsE => -[W [oW Wr]]; exact.
 Qed.
 
@@ -400,9 +415,9 @@ Lemma within_interior (x : T) : A° x -> within A (nbhs x) = nbhs x.
 Proof.
 move=> Aox; rewrite eqEsubset; split; last exact: cvg_within.
 rewrite ?nbhsE => W /= => [[B + BsubW]].
-rewrite open_nbhsE => [[oB nbhsB]].
+rewrite mem_openE => [[oB nbhsB]].
 exists (B `&` A°); last by move=> t /= [] /BsubW + /interior_subset; apply.
-rewrite open_nbhsE; split; first by apply: openI => //; exact: open_interior.
+rewrite mem_openE; split; first by apply: openI => //; exact: open_interior.
 by apply: filterI => //; have := open_interior A; rewrite openE; exact.
 Qed.
 
@@ -658,14 +673,14 @@ Qed.
 (** meets *)
 
 Lemma meets_openr {T : topologicalType} (F : set_system T) (x : T) :
-  F `#` nbhs x = F `#` open_nbhs x.
+  F `#` nbhs x = F `#` mem_open x.
 Proof.
-rewrite propeqE; split; [exact/meetsSr/open_nbhs_nbhs|].
+rewrite propeqE; split; [exact/meetsSr/mem_open_nbhs|].
 by move=> P A B {}/P P; rewrite nbhsE => -[B' /P + sB]; apply: subsetI_neq0.
 Qed.
 
 Lemma meets_openl {T : topologicalType} (F : set_system T) (x : T) :
-  nbhs x `#` F = open_nbhs x `#` F.
+  nbhs x `#` F = mem_open x `#` F.
 Proof. by rewrite meetsC meets_openr meetsC. Qed.
 (** Closed sets in topological spaces *)
 
@@ -678,11 +693,11 @@ Definition closure (A : set T) :=
 Lemma closureEnbhs A : closure A = [set p | globally A `#` nbhs p].
 Proof. by under eq_fun do rewrite meets_globallyl. Qed.
 
-Lemma closureEonbhs A : closure A = [set p | globally A `#` open_nbhs p].
+Lemma closureEonbhs A : closure A = [set p | globally A `#` mem_open p].
 Proof. by under eq_fun do rewrite -meets_openr meets_globallyl. Qed.
 
 Lemma subset_closure (A : set T) : A `<=` closure A.
-Proof. by move=> p ??; exists p; split=> //; apply: nbhs_singleton. Qed.
+Proof. by move=> p ??; exists p; split=> //; exact: nbhs_singleton. Qed.
 
 Lemma closure_eq0 (A : set T) : closure A = set0 -> A = set0.
 Proof.
@@ -704,7 +719,7 @@ by rewrite propeqE; split => [[/eqP ? ?]|[[? /eqP ?]]]; do 2?split.
 Qed.
 
 Lemma limit_pointEonbhs E :
-  limit_point E = [set p | globally (E `\ p) `#` open_nbhs p].
+  limit_point E = [set p | globally (E `\ p) `#` mem_open p].
 Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed.
 
 Lemma subset_limit_point E : limit_point E `<=` closure E.
@@ -896,7 +911,7 @@ Qed.
 End closure_lemmas.
 
 Section regular_open_closed.
-Variable T : topologicalType.
+Context {T : topologicalType}.
 
 Definition regopen (A : set T) := (closure A)° = A.
 
@@ -905,14 +920,14 @@ Definition regclosed (A : set T) := closure (A°) = A.
 End regular_open_closed.
 
 Section closure_interior_lemmas.
-Variable T : topologicalType.
+Context {T : topologicalType}.
 Implicit Types (A B : set T).
 
 Lemma interiorC A : (~` A)° = ~` closure A.
 Proof.
 rewrite eqEsubset; split=> x; rewrite /closure /interior nbhsE /= -existsNE.
   case=> U ? /disjoints_subset UA; exists U; rewrite not_implyE.
-  split; first exact/open_nbhs_nbhs.
+  split; first exact/mem_open_nbhs.
   by rewrite setIC UA; apply/set0P; rewrite eqxx.
 case=> X; rewrite not_implyE nbhsE=> -[] -[] U xU UX AX0.
 exists U => //; apply/(subset_trans UX)/disjoints_subset; rewrite setIC.
@@ -995,15 +1010,15 @@ End closure_interior_lemmas.
 #[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `closureC`")]
 Notation closure_setC := closureC (only parsing).
 
-Definition dense (T : topologicalType) (S : set T) :=
-  forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.
+Definition dense {T : topologicalType} (S : set T) :=
+  forall O : set T, O !=set0 -> open O -> O `&` S !=set0.
 
-Lemma denseNE (T : topologicalType) (S : set T) : ~ dense S ->
-  exists O, (exists x, open_nbhs x O) /\ (O `&` S = set0).
+Lemma denseNE {T : topologicalType} (S : set T) : ~ dense S ->
+  exists2 O, (exists x, mem_open x O) & (O `&` S = set0).
 Proof.
-rewrite /dense /open_nbhs.
+rewrite /dense /mem_open.
 move=> /existsNP[X /not_implyP[[x Xx] /not_implyP[ Ox /forallNP A]]].
-by exists X; split; [exists x | rewrite -subset0; apply/A].
+by exists X; [exists x | rewrite -subset0; apply/A].
 Qed.
 
 Lemma denseI (T : topologicalType) (A B : set T) :
diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v
index 1354101134..9f93f73983 100644
--- a/theories/topology_theory/uniform_structure.v
+++ b/theories/topology_theory/uniform_structure.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra all_classical.
 From mathcomp Require Import topology_structure.
@@ -318,13 +318,16 @@ exists (range f); split; first exact: card_image_le.
 by move=> E /fsubE [n fnA]; exists (f n) => //; exists n.
 Qed.
 
-Lemma open_nbhs_entourage (U : uniformType) (x : U) (A : set (U * U)) :
-  entourage A -> open_nbhs x (xsection A x)°.
+Lemma entourage_mem_open {U : uniformType} (x : U) (A : set (U * U)) :
+  entourage A -> mem_open x (xsection A x)°.
 Proof.
 move=> entA; split; first exact: open_interior.
 by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhs_entourage.
 Qed.
 
+#[deprecated(since="mathcomp-analysis 1.18.0", use=entourage_mem_open)]
+Notation open_nbhs_entourage := entourage_mem_open (only parsing).
+
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
   (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.
 
@@ -356,9 +359,6 @@ HB.mixin Record Uniform_isComplete T & PointedUniform T := {
 HB.structure Definition Complete :=
   {T of Uniform T & Uniform_isComplete T & isPointed T}.
 
-#[deprecated(since="mathcomp-analysis 2.0", note="use cauchy_cvg instead")]
-Notation complete_ax := cauchy_cvg (only parsing).
-
 Section completeType1.
 
 Context {T : completeType}.