open_nbhs -> mem_open

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

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]) => //.

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 /=.

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,15 +762,15 @@ 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.
 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)//.

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//.

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.

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.

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}.

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.

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.

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.

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.

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 _ _)).

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.