diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 98def5d2e..496ab1bb9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -83,6 +83,54 @@
   + lemma `maxe_cvg_0_cvg_fin_num`
   + lemma `maxe_cvg_maxr_cvg`
   + lemma `maxe_cvg_0_cvg_0`
+- in `constructive_ereal.v`
+  + lemma `lee_subgt0Pr`
+
+- in `topology.v`:
+  + lemma `nbhs_dnbhs_neq`
+
+- in `normedtype.v`:
+  + lemma `not_near_at_rightP`
+
+- in `realfun.v`:
+  + lemma `cvg_at_right_left_dnbhs`
+  + lemma `cvg_at_rightP`
+  + lemma `cvg_at_leftP`
+  + lemma `cvge_at_rightP`
+  + lemma `cvge_at_leftP`
+  + lemma `lime_sup`
+  + lemma `lime_inf`
+  + lemma `lime_supE`
+  + lemma `lime_infE`
+  + lemma `lime_infN`
+  + lemma `lime_supN`
+  + lemma `lime_sup_ge0`
+  + lemma `lime_inf_ge0`
+  + lemma `lime_supD`
+  + lemma `lime_sup_le`
+  + lemma `lime_inf_sup`
+  + lemma `lim_lime_inf`
+  + lemma `lim_lime_sup`
+  + lemma `lime_sup_inf_at_right`
+  + lemma `lime_sup_inf_at_left`
+
+- in `normedtype.v`:
+  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
+  + lemma `dnbhsN`
+  + lemma `limf_esup_dnbhsN`
+
+- in `topology.v`:
+  + lemma `dnbhs_ball`
+
+- in `normedtype.v`
+  + definitions `limf_esup`, `limf_einf`
+  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
+
+- in `sequences.v`:
+  + lemmas `limn_esup_lim`, `limn_einf_lim`
+
+- in `realfun.v`:
+  + lemmas `lime_sup_lim`, `lime_inf_lim`
 
 ### Changed
 
@@ -118,6 +166,10 @@
 - moved from `topology.v` to `mathcomp_extra.v`
   + definition `monotonous`
 
+- in `sequences.v`:
+  + `limn_esup` now defined from `lime_sup`
+  + `limn_einf` now defined from `limn_esup`
+  
 ### Renamed
 
 - in `exp.v`:
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 070dc5075..9905fb342 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -3035,6 +3035,14 @@ apply/(iffP idP) => [|].
   by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
 Qed.
 
+Lemma lee_subgt0Pr x y :
+  reflect (forall e, (0 < e)%R -> x - e%:E <= y) (x <= y).
+Proof.
+apply/(iffP idP) => [xy e|xy].
+  by rewrite lee_subl_addr//; move: e; exact/lee_addgt0Pr.
+by apply/lee_addgt0Pr => e e0; rewrite -lee_subl_addr// xy.
+Qed.
+
 Lemma lee_mul01Pr x y : 0 <= x ->
   reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y).
 Proof.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index a51e63bf3..d41288538 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -2370,7 +2370,8 @@ pose g n := fun x => einfs (f ^~ x) n.
 have mg := measurable_fun_einfs mf.
 have g0 n x : D x -> 0 <= g n x.
   by move=> Dx; apply: lb_ereal_inf => _ [m /= nm <-]; exact: f0.
-rewrite monotone_convergence //; last first.
+under eq_integral do rewrite limn_einf_lim.
+rewrite limn_einf_lim monotone_convergence //; last first.
   move=> x Dx m n mn /=; apply: le_ereal_inf => _ /= [p /= np <-].
   by exists p => //=; rewrite (leq_trans mn).
 apply: lee_lim.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 45622b50e..f0cdb617e 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1823,7 +1823,7 @@ Proof.
 move=> mf mD; rewrite (_ :  (fun _ => _) =
     (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])).
   by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups.
-rewrite funeqE => t; apply/cvg_lim => //.
+rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //.
 rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))).
   exact: cvg_esups_inf.
 by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
@@ -1834,6 +1834,7 @@ Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) :
   (forall x, D x -> f_ ^~ x --> f x) -> measurable_fun D f.
 Proof.
 move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x).
+  rewrite limn_esup_lim.
   by move=> Dx; have /cvg_lim  <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx).
 apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //.
   by move=> x; rewrite inE => Dx; rewrite fE.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 7b871baf9..d947bd320 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -10,6 +10,11 @@ Require Import ereal reals signed topology prodnormedzmodule.
 (*                                                                            *)
 (* Note that balls in topology.v are not necessarily open, here they are.     *)
 (*                                                                            *)
+(* * Limit superior and inferior:                                             *)
+(*   limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F    *)
+(*                                   f has type X -> \bar R.                  *)
+(*                                   F has type set (set X).                  *)
+(*                                                                            *)
 (* * Normed Topological Abelian groups:                                       *)
 (*  pseudoMetricNormedZmodType R  == interface type for a normed topological  *)
 (*                                   Abelian group equipped with a norm       *)
@@ -144,6 +149,35 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+Section limf_esup_einf.
+Variables (T : choiceType) (X : filteredType T) (R : realFieldType).
+Implicit Types (f : X -> \bar R) (F : set (set X)).
+Local Open Scope ereal_scope.
+
+Definition limf_esup f F := ereal_inf [set ereal_sup (f @` V) | V in F].
+
+Definition limf_einf f F := - limf_esup (\- f) F.
+
+Lemma limf_esupE f F :
+  limf_esup f F = ereal_inf [set ereal_sup (f @` V) | V in F].
+Proof. by []. Qed.
+
+Lemma limf_einfE f F :
+  limf_einf f F = ereal_sup [set ereal_inf (f @` V) | V in F].
+Proof.
+rewrite /limf_einf limf_esupE /ereal_inf oppeK -[in RHS]image_comp /=.
+congr (ereal_sup [set _ | _ in [set ereal_sup _ | _ in _]]).
+by under eq_fun do rewrite -image_comp.
+Qed.
+
+Lemma limf_esupN f F : limf_esup (\- f) F = - limf_einf f F.
+Proof. by rewrite /limf_einf oppeK. Qed.
+
+Lemma limf_einfN f F : limf_einf (\- f) F = - limf_esup f F.
+Proof. by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed.
+
+End limf_esup_einf.
+
 Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0.
 
 Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K)
@@ -214,6 +248,20 @@ move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
 by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
 Qed.
 
+Lemma dnbhsN {R : numFieldType} (r : R) :
+  (- r)%R^' = (fun A => -%R @` A) @` r^'.
+Proof.
+apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
+  exists (-%R @` A).
+    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
+    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
+  by rewrite opprK.
+exists e => //= x/=; rewrite -opprD normrN => axe xa.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+by rewrite opprK.
+Qed.
+
 Module PseudoMetricNormedZmodule.
 Section ClassDef.
 Variable R : numDomainType.
@@ -1629,6 +1677,15 @@ End Exports.
 End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
+Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) :
+  limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'.
+Proof.
+rewrite /limf_esup dnbhsN image_comp/=.
+congr (ereal_inf [set _ | _ in _]); apply/funext => A /=.
+rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=.
+by rewrite opprK.
+Qed.
+
 Section NormedModule_numDomainType.
 Variables (R : numDomainType) (V : normedModType R).
 
@@ -2077,6 +2134,47 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y.
 Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
 Unshelve. all: by end_near. Qed.
 
+Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) :
+  ~ (\forall x \near p^'+, P (f x)) ->
+  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x).
+Proof.
+move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
+apply: contrapT; apply: pePf; apply/andP; split.
+- by near: t; exact: nbhs_right_gt.
+- by near: t; apply: nbhs_right_lt; rewrite ltr_addl.
+Unshelve. all: by end_near. Qed.
+
+Lemma withinN (A : set R) a :
+  within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)].
+Proof.
+rewrite eqEsubset /=; split; move=> E /= [e e0 aeE]; exists e => //.
+  move=> r are ra; apply: aeE; last by rewrite memNE opprK.
+  by rewrite /= opprK addrC distrC.
+move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE.
+by rewrite /= opprK -normrN opprD.
+Qed.
+
+Let fun_predC (T : choiceType) (f : T -> T) (p : pred T) : involutive f ->
+  [set f x | x in p] = [set x | x in p \o f].
+Proof.
+by move=> fi; apply/seteqP; split => _/= [y hy <-];
+  exists (f y) => //; rewrite fi.
+Qed.
+
+Lemma at_rightN a : (- a)^'+ = -%R @ a^'-.
+Proof.
+rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+Qed.
+
+Lemma at_leftN a : (- a)^'- = -%R @ a^'+.
+Proof.
+rewrite /at_left withinN [X in within X _](_ : _ = [set u | a < u])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -2088,6 +2186,20 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma cvg_at_leftNP {T : topologicalType} {R : numFieldType}
+    (f : R -> T) a (l : T) :
+  f @ a^'- --> l <-> f \o -%R @ (- a)^'+ --> l.
+Proof.
+by rewrite at_rightN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
+Qed.
+
+Lemma cvg_at_rightNP {T : topologicalType} {R : numFieldType}
+    (f : R -> T) a (l : T) :
+  f @ a^'+ --> l <-> f \o -%R @ (- a)^'- --> l.
+Proof.
+by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
+Qed.
+
 Section open_itv_subset.
 Context {R : realType}.
 Variables (A : set R) (x : R).
diff --git a/theories/realfun.v b/theories/realfun.v
index b84a816cc..0e165d108 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -4,7 +4,7 @@ From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
 Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
-Require Import real_interval.
+Require Import sequences real_interval.
 From HB Require Import structures.
 
 (******************************************************************************)
@@ -19,6 +19,10 @@ From HB Require Import structures.
 (*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
 (*                                        continuous up to the boundary       *)
 (*                                                                            *)
+(* * Limit superior and inferior for functions:                               *)
+(*   lime_sup f a/lime_inf f a == limit sup/inferior of the extended real-    *)
+(*                                valued function f at point a                *)
+(*                                                                            *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -80,8 +84,135 @@ apply: near_eq_cvg; near do rewrite subrK; exists M.
 by rewrite num_real.
 Unshelve. all: by end_near. Qed.
 
+Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) :
+  f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l ->
+  f x @[x --> p^'] --> l.
+Proof.
+move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
+have {fppl}[a /= a0 fppl] := fppl _ e0; have {fpnl}[b /= b0 fpnl] := fpnl _ e0.
+near=> t.
+have : t != p by near: t; exact: nbhs_dnbhs_neq.
+rewrite neq_lt => /orP[tp|pt].
+- apply: fpnl => //=; near: t.
+  exists (b / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivr_mulr// ler_pmulr// ler1n.
+- apply: fppl =>//=; near: t.
+  exists (a / 2) => //=; first by rewrite divr_gt0.
+  move=> z/= + _ => /lt_le_trans; apply.
+  by rewrite ler_pdivr_mulr// ler_pmulr// ler1n.
+Unshelve. all: by end_near. Qed.
+
 End fun_cvg_realFieldType.
 
+Section cvgr_fun_cvg_seq.
+Context {R : realType}.
+
+Lemma cvg_at_rightP (f : R -> R) (p l : R) :
+  f x @[x --> p^'+] --> l <->
+  (forall u : R^nat, (forall n, u n > p) /\ (u --> p) ->
+    f (u n) @[n --> \oo] --> l).
+Proof.
+split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt ucvg]|pfl].
+  apply/cvgrPdist_le => e e0.
+  have [r /= r0 {}fpl] := fpl _ e0; have [s /= s0 {}ucvg] := ucvg _ r0.
+  near=> t; apply: fpl => //=; apply: ucvg => /=.
+  by near: t; exists s.
+apply: contrapT => fpl; move: pfl; apply/existsNP.
+suff: exists2 x : R ^nat,
+    (forall k, x k > p) /\ x --> p & ~ f (x n) @[n --> \oo] --> l.
+  by move=> [x_] h; exists x_; exact/not_implyP.
+have [e He] : exists e : {posnum R}, forall d : {posnum R},
+    exists xn : R, [/\ xn > p, `|xn - p| < d%:num & `|f xn - l| >= e%:num].
+  apply: contrapT; apply: contra_not fpl => /forallNP h.
+  apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0).
+  move/forallNP => {}h; near=> t.
+  have /not_and3P[abs|abs|/negP] := h t.
+  - by exfalso; apply: abs; near: t; exact: nbhs_right_gt.
+  - exfalso; apply: abs.
+    by near: t;  by exists d%:num => //= z/=; rewrite distrC.
+  - by rewrite -ltNge distrC => /ltW.
+have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
+exists (fun n => sval (cid (He (PosNum (invn n))))).
+  split => [k|]; first by rewrite /sval/=; case: cid => x [].
+  apply/cvgrPdist_lt => r r0; near=> t.
+  rewrite /sval/=; case: cid => x [px xpt _].
+  rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pinv ?posrE ?invr_gt0//.
+  near: t; exists `|ceil (r^-1)|%N => // s /=.
+  rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans.
+  by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge.
+move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
+rewrite /sval/=; case: cid => // x [px xpn].
+by rewrite leNgt distrC => /negP.
+Unshelve. all: by end_near. Qed.
+
+Lemma cvg_at_leftP (f : R -> R) (p l : R) :
+  f x @[x --> p^'-] --> l <->
+  (forall u : R^nat, (forall n, u n < p) /\ (u --> p) ->
+    f (u n) @[n --> \oo] --> l).
+Proof.
+apply: (iff_trans (cvg_at_leftNP f p l)).
+apply: (iff_trans (cvg_at_rightP _ _ _)).
+split=> [pfl u [pu up]|pfl u [pu up]].
+  rewrite -(opprK u); apply: pfl.
+  by split; [move=> k; rewrite ltr_oppr opprK//|exact/cvgNP].
+apply: pfl.
+by split; [move=> k; rewrite ltr_oppl//|apply/cvgNP => /=; rewrite opprK].
+Qed.
+
+End cvgr_fun_cvg_seq.
+
+Section cvge_fun_cvg_seq.
+Context {R : realType}.
+
+Lemma cvge_at_rightP (f : R -> \bar R) (p l : R) :
+  f x @[x --> p^'+] --> l%:E <->
+  (forall u : R^nat, (forall n, u n > p) /\ u --> p ->
+    f (u n) @[n --> \oo] --> l%:E).
+Proof.
+split=> [/fine_cvgP [ffin_num fpl] u [pu up]|h].
+  apply/fine_cvgP; split; last by move/cvg_at_rightP : fpl; exact.
+  have [e /= e0 {}ffin_num] := ffin_num.
+  move/cvgrPdist_lt : up => /(_ _ e0)[s /= s0 {}up]; near=> t.
+  by apply: ffin_num => //=; apply: up => /=; near: t; exists s.
+suff H : \forall F \near p^'+, f F \is a fin_num.
+  by apply/fine_cvgP; split => //; apply/cvg_at_rightP => u /h /fine_cvgP[].
+apply: contrapT => /not_near_at_rightP abs.
+have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
+pose y_ n := sval (cid2 (abs (PosNum (invn n)))).
+have py_ k : p < y_ k by rewrite /y_ /sval/=; case: cid2 => //= x /andP[].
+have y_p : y_ --> p.
+  apply/cvgrPdist_lt => e e0; near=> t.
+  rewrite ltr0_norm// ?subr_lt0// opprB.
+  rewrite /y_ /sval/=; case: cid2 => //= x /andP[_ + _].
+  rewrite ltr_subl_addr => /lt_le_trans; apply.
+  rewrite addrC ler_add2r -(invrK e) lef_pinv// ?posrE ?invr_gt0//.
+  near: t.
+  exists `|ceil e^-1|%N => // k /= ek.
+  rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//.
+    by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW.
+  by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW.
+have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p).
+near \oo => n.
+have mn : (m <= n)%N by near: n; exists m.
+have {mn} := mfy_ _ mn.
+rewrite /y_ /sval; case: cid2 => /= x _.
+Unshelve. all: by end_near. Qed.
+
+Lemma cvge_at_leftP (f : R -> \bar R) (p l : R) :
+  f x @[x --> p^'-] --> l%:E <->
+  (forall u : R^nat, (forall n, u n < p) /\ u --> p ->
+    f (u n) @[n --> \oo] --> l%:E).
+Proof.
+apply: (iff_trans (cvg_at_leftNP f p l%:E)).
+apply: (iff_trans (cvge_at_rightP _ _ l)); split=> h u [up pu].
+- rewrite (_ : u = \- (\- u))%R; last by apply/funext => ?/=; rewrite opprK.
+  by apply: h; split; [by move=> n; rewrite ltr_oppl opprK|exact: cvgN].
+- by apply: h; split => [n|]; [rewrite ltr_oppl|move/cvgN : pu; rewrite opprK].
+Qed.
+
+End cvge_fun_cvg_seq.
+
 Section fun_cvg_realType.
 Context {R : realType}.
 
@@ -393,6 +524,301 @@ End fun_cvg_ereal.
 
 End fun_cvg.
 
+Section lime_sup_inf.
+Variable R : realType.
+Local Open Scope ereal_scope.
+Implicit Types (f g : R -> \bar R) (a r s l : R).
+
+Definition lime_sup f a : \bar R := limf_esup f a^'.
+
+Definition lime_inf f a : \bar R := - lime_sup (\- f) a.
+
+Let sup_ball f a r := ereal_sup [set f x | x in ball a r `\ a].
+
+Let sup_ball_le f a r s : (r <= s)%R -> sup_ball f a r <= sup_ball f a s.
+Proof.
+move=> rs; apply: ub_ereal_sup => /= _ /= [t [rt ta] <-].
+by apply: ereal_sup_ub => /=; exists t => //; split => //; exact: le_ball rt.
+Qed.
+
+Let sup_ball_is_cvg f a : cvg (sup_ball f a e @[e --> 0^'+]).
+Proof.
+apply: nondecreasing_at_right_is_cvge => x.
+by rewrite in_itv/= andbT => x0 y /sup_ball_le.
+Qed.
+
+Let inf_ball f a r := - sup_ball (\- f) a r.
+
+Let inf_ballE f a r : inf_ball f a r = ereal_inf [set f x | x in ball a r `\ a].
+Proof.
+by rewrite /inf_ball /ereal_inf; congr (- _); rewrite /sup_ball -image_comp.
+Qed.
+
+Let inf_ball_le f a r s : (s <= r)%R -> inf_ball f a r <= inf_ball f a s.
+Proof. by move=> sr; rewrite /inf_ball lee_oppl oppeK sup_ball_le. Qed.
+
+Let inf_ball_is_cvg f a : cvg (inf_ball f a e @[e --> 0^'+]).
+Proof.
+apply: nonincreasing_at_right_is_cvge => //.
+by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le.
+Qed.
+
+Let le_sup_ball f g a :
+  (forall r, (0 < r)%R -> forall y : R, y != a -> ball a r y -> f y <= g y) ->
+  \forall r \near 0^'+, sup_ball f a r <= sup_ball g a r.
+Proof.
+move=> fg; near=> r; apply: ub_ereal_sup => /= _ [s [pas /= /eqP ps]] <-.
+apply: (@le_trans _ _ (g s)); first exact: (fg r).
+by apply: ereal_sup_ub => /=; exists s => //; split => //; exact/eqP.
+Unshelve. all: by end_near. Qed.
+
+Lemma lime_sup_lim f a : lime_sup f a = lim (sup_ball f a e @[e --> 0^'+]).
+Proof.
+apply/eqP; rewrite eq_le; apply/andP; split.
+  apply: lime_ge => //; near=> e; apply: ereal_inf_lb => /=.
+  by exists (ball a e `\ a) => //=; exact: dnbhs_ball.
+apply: lb_ereal_inf => /= _ [A [r /= r0 arA] <-].
+apply: lime_le => //; near=> e.
+apply: le_ereal_sup => _ [s [ase /eqP sa] <- /=].
+exists s => //; apply: arA => //=; apply: (lt_le_trans ase).
+by near: e; exact: nbhs_right_le.
+Unshelve. all: by end_near. Qed.
+
+Lemma lime_inf_lim f a : lime_inf f a = lim (inf_ball f a e @[e --> 0^'+]).
+Proof.
+rewrite /lime_inf lime_sup_lim -limeN; last exact: sup_ball_is_cvg.
+by rewrite /sup_ball; under eq_fun do rewrite -image_comp.
+Qed.
+
+Lemma lime_supE f a :
+  lime_sup f a = ereal_inf [set sup_ball f a e | e in `]0, +oo[ ]%R.
+Proof.
+rewrite lime_sup_lim; apply/cvg_lim => //.
+apply: nondecreasing_at_right_cvge => //.
+by move=> x; rewrite in_itv/= andbT => x0 y; exact: sup_ball_le.
+Qed.
+
+Lemma lime_infE f a :
+  lime_inf f a = ereal_sup [set inf_ball f a e | e in `]0, +oo[ ]%R.
+Proof. by rewrite /lime_inf lime_supE /ereal_inf oppeK image_comp. Qed.
+
+Lemma lime_infN f a : lime_inf (\- f) a = - lime_sup f a.
+Proof. by rewrite /lime_sup -limf_einfN. Qed.
+
+Lemma lime_supN f a : lime_sup (\- f) a = - lime_inf f a.
+Proof. by rewrite /lime_inf oppeK. Qed.
+
+Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a.
+Proof.
+move=> f0; rewrite lime_supE; apply: lb_ereal_inf => /= x [e /=].
+rewrite in_itv/= andbT => e0 <-{x}; rewrite -(ereal_sup1 0) ereal_sup_le //=.
+exists (f (a + e / 2)%R); last by rewrite ereal_sup1 f0.
+exists (a + e / 2)%R => //=; split.
+  rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//.
+  by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n.
+by apply/eqP; rewrite gt_eqF// ltr_spaddr// divr_gt0.
+Qed.
+
+Lemma lime_inf_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_inf f a.
+Proof.
+move=> f0; rewrite lime_inf_lim; apply: lime_ge; first exact: inf_ball_is_cvg.
+near=> b; rewrite inf_ballE.
+by apply: lb_ereal_inf => /= _ [r [abr/= ra]] <-; exact: f0.
+Unshelve. all: by end_near. Qed.
+
+Lemma lime_supD f g a : lime_sup f a +? lime_sup g a ->
+  lime_sup (f \+ g)%E a <= lime_sup f a + lime_sup g a.
+Proof.
+move=> fg; rewrite !lime_sup_lim -limeD//; last first.
+  by rewrite -!lime_sup_lim.
+apply: lee_lim => //.
+- apply: nondecreasing_at_right_is_cvge => x.
+  by rewrite in_itv/= andbT => x0 y xy; rewrite lee_add//; exact: sup_ball_le.
+- near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-.
+  by apply: lee_add; apply: ereal_sup_ub => /=; exists a1.
+Unshelve. all: by end_near. Qed.
+
+Lemma lime_sup_le f g a :
+  (forall r, (0 < r)%R -> forall y, y != a -> ball a r y -> f y <= g y) ->
+  lime_sup f a <= lime_sup g a.
+Proof.
+by move=> fg; rewrite !lime_sup_lim; apply: lee_lim => //; exact: le_sup_ball.
+Qed.
+
+Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a.
+Proof.
+rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //.
+near=> r.
+rewrite ereal_sup_le//.
+have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R.
+  exists (a + r / 2)%R => //;  split.
+    rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//.
+    by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n.
+  by apply/eqP; rewrite gt_eqF// ltr_spaddr// divr_gt0.
+by exists (f (a + r / 2)%R) => //=; rewrite inf_ballE ereal_inf_lb.
+Unshelve. all: by end_near. Qed.
+
+Local Lemma lim_lime_sup' f a (l : R) :
+  f r @[r --> a] --> l%:E -> lime_sup f a <= l%:E.
+Proof.
+move=> fpA; apply/lee_addgt0Pr => e e0; rewrite lime_sup_lim.
+apply: lime_le => //.
+move/fine_cvg : (fpA) => /cvgrPdist_le fpA1.
+move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2.
+have := fpA1 _ e0 => -[q /= q0] H.
+near=> x.
+apply: ub_ereal_sup => //= _ [y [pry /= yp <-]].
+have ? : f y \is a fin_num.
+  apply: fpA2.
+  rewrite /ball_ /= (lt_le_trans pry)//.
+  by near: x; exact: nbhs_right_le.
+rewrite -lee_subel_addl// -(@fineK _ (f y)) // -EFinB lee_fin.
+rewrite (le_trans (ler_norm _))// distrC H// /ball_/= ltr_distlC.
+move: pry; rewrite /ball/= ltr_distlC => /andP[pay ypa].
+have xq : (x <= q)%R by near: x; exact: nbhs_right_le.
+apply/andP; split.
+  by rewrite (le_lt_trans _ pay)// ler_sub.
+by rewrite (lt_le_trans ypa)// ler_add2l.
+Unshelve. all: by end_near.
+Qed.
+
+Local Lemma lim_lime_inf' f a (l : R) :
+  f r @[r --> a] --> l%:E -> l%:E <= lime_inf f a.
+Proof.
+move=> fpA; apply/lee_subgt0Pr => e e0; rewrite lime_inf_lim.
+apply: lime_ge => //.
+move/fine_cvg : (fpA) => /cvgrPdist_le fpA1.
+move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2.
+have := fpA1 _ e0 => -[q /= q0] H.
+near=> x.
+rewrite inf_ballE.
+apply: lb_ereal_inf => //= _ [y [pry /= yp <-]].
+have ? : f y \is a fin_num.
+  apply: fpA2.
+  rewrite /ball_ /= (lt_le_trans pry)//.
+  by near: x; exact: nbhs_right_le.
+rewrite -(@fineK _ (f y)) // -EFinB lee_fin ler_subl_addr -ler_subl_addl.
+rewrite (le_trans (ler_norm _))// H// /ball_/= ltr_distlC.
+move: pry; rewrite /ball/= ltr_distlC => /andP[pay ypa].
+have xq : (x <= q)%R by near: x; exact: nbhs_right_le.
+apply/andP; split.
+  by rewrite (le_lt_trans _ pay)// ler_sub.
+by rewrite (lt_le_trans ypa)// ler_add2l.
+Unshelve. all: by end_near.
+Qed.
+
+Lemma lim_lime_inf f a (l : R) :
+  f r @[r --> a] --> l%:E -> lime_inf f a = l%:E.
+Proof.
+move=> h; apply/eqP; rewrite eq_le.
+by rewrite lim_lime_inf'// andbT (le_trans (lime_inf_sup _ _))// lim_lime_sup'.
+Qed.
+
+Lemma lim_lime_sup f a (l : R) :
+  f r @[r --> a] --> l%:E -> lime_sup f a = l%:E.
+Proof.
+move=> h; apply/eqP; rewrite eq_le.
+by rewrite lim_lime_sup'//= (le_trans _ (lime_inf_sup _ _))// lim_lime_inf'.
+Qed.
+
+Local Lemma lime_supP f a l :
+  lime_sup f a = l%:E -> forall e : {posnum R}, exists d : {posnum R},
+  forall x, (ball a d%:num `\ a) x -> f x < l%:E + e%:num%:E.
+Proof.
+rewrite lime_supE => fal.
+have H (e : {posnum R}) :
+    exists d : {posnum R}, l%:E <= sup_ball f a d%:num < l%:E + e%:num%:E.
+  apply: contrapT => /forallNP H.
+  have : ereal_inf [set sup_ball f a r | r in `]0%R, +oo[] \is a fin_num.
+    by rewrite fal.
+  move=> /lb_ereal_inf_adherent-/(_ e%:num ltac:(by []))[y] /=.
+  case=> r; rewrite in_itv/= andbT => r0 <-{y}.
+  rewrite ltNge => /negP; apply.
+  have /negP := H (PosNum r0).
+  rewrite negb_and => /orP[|].
+    rewrite -ltNge => farl.
+    have : ereal_inf [set sup_ball f a r | r in `]0%R, +oo[] < l%:E.
+      rewrite (le_lt_trans _ farl)//; apply: ereal_inf_lb => /=; exists r => //.
+      by rewrite in_itv/= r0.
+    by rewrite fal ltxx.
+  by rewrite -leNgt; apply: le_trans; rewrite lee_add2r// fal.
+move=> e; have [d /andP[lfp fpe]] := H e.
+exists d => r /= [] prd rp.
+by rewrite (le_lt_trans _ fpe)//; apply: ereal_sup_ub => /=; exists r.
+Qed.
+
+Local Lemma lime_infP f a l :
+  lime_inf f a = l%:E -> forall e : {posnum R}, exists d : {posnum R},
+  forall x, (ball a d%:num `\ a) x -> l%:E - e%:num%:E < f x.
+Proof.
+move=> /(congr1 oppe); rewrite -lime_supN => /lime_supP => H e.
+have [d {}H] := H e.
+by exists d => r /H; rewrite lte_oppl oppeD// EFinN oppeK.
+Qed.
+
+Lemma lime_sup_inf_at_right f a l :
+  lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'+] --> l%:E.
+Proof.
+move=> supfpl inffpl; apply/cvge_at_rightP => u [pu up].
+have fu : \forall n \near \oo, f (u n) \is a fin_num.
+  have [dsup Hdsup] := lime_supP supfpl (PosNum ltr01).
+  have [dinf Hdinf] := lime_infP inffpl (PosNum ltr01).
+  near=> n; rewrite fin_numE; apply/andP; split.
+    apply/eqP => fxnoo.
+    suff : (ball a dinf%:num `\ a) (u n) by move=> /Hdinf; rewrite fxnoo.
+    split; last by apply/eqP; rewrite gt_eqF.
+    by near: n; move/cvgrPdist_lt : up; exact.
+  apply/eqP => fxnoo.
+  suff : (ball a dsup%:num `\ a) (u n) by move=> /Hdsup; rewrite fxnoo.
+  split; last by apply/eqP; rewrite gt_eqF.
+  by near: n; move/cvgrPdist_lt : up; exact.
+apply/fine_cvgP; split => /=; first exact: fu.
+apply/cvgrPdist_le => _/posnumP[e].
+have [d1 Hd1] : exists d1 : {posnum R},
+    l%:E - e%:num%:E <= ereal_inf [set f x | x in ball a d1%:num `\ a].
+  have : l%:E - e%:num%:E < lime_inf f a.
+    by rewrite inffpl lte_subl_addr// lte_addl.
+  rewrite lime_infE => /ereal_sup_gt[x /= [r]]; rewrite in_itv/= andbT.
+  move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW//.
+  by rewrite -inf_ballE.
+have [d2 Hd2] : exists d2 : {posnum R},
+    ereal_sup [set f x | x in ball a d2%:num `\ a] <= l%:E + e%:num%:E.
+  have : lime_sup f a < l%:E + e%:num%:E by rewrite supfpl lte_addl.
+  rewrite lime_supE => /ereal_inf_lt[x /= [r]]; rewrite in_itv/= andbT.
+  by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW.
+pose d := minr d1%:num d2%:num.
+have d0 : (0 < d)%R by rewrite lt_minr; apply/andP; split => //=.
+move/cvgrPdist_lt : up => /(_ _ d0)[m _] {}ucvg.
+near=> n.
+rewrite /= ler_distlC; apply/andP; split.
+  rewrite -lee_fin EFinB (le_trans Hd1)//.
+  rewrite (@le_trans _ _ (ereal_inf [set f x | x in ball a d `\ a]))//.
+    apply: le_ereal_inf => _/= [r [adr ra] <-]; exists r => //; split => //.
+    by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx.
+  apply: ereal_inf_lb => /=; exists (u n).
+    split; last by apply/eqP; rewrite eq_sym lt_eqF.
+    by apply: ucvg => //=; near: n; by exists m.
+  by rewrite fineK//; by near: n.
+rewrite -lee_fin EFinD (le_trans _ Hd2)//.
+rewrite (@le_trans _ _ (ereal_sup [set f x | x in ball a d `\ a]))//; last first.
+  apply: le_ereal_sup => z/= [r [adr rp] <-{z}]; exists r => //; split => //.
+  by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx orbT.
+apply: ereal_sup_ub => /=; exists (u n).
+  split; last by apply/eqP; rewrite eq_sym lt_eqF.
+  by apply: ucvg => //=; near: n; exists m.
+by rewrite fineK//; near: n.
+Unshelve. all: by end_near. Qed.
+
+Lemma lime_sup_inf_at_left f a l :
+  lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'-] --> l%:E.
+Proof.
+move=> supfal inffal; apply/cvg_at_leftNP/lime_sup_inf_at_right.
+- by rewrite /lime_sup -limf_esup_dnbhsN.
+- by rewrite /lime_inf /lime_sup -(limf_esup_dnbhsN (-%E \o f)) limf_esupN oppeK.
+Qed.
+
+End lime_sup_inf.
+
 Section derivable_oo_continuous_bnd.
 Context {R : numFieldType} {V : normedModType R}.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index de8d8055a..10e12190a 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -69,14 +69,15 @@ Require Import reals ereal signed topology normedtype landau.
 (*   positive) extended numbers use the string "nneseries" (resp. "npeseries")*)
 (*   as part of their identifier                                              *)
 (*                                                                            *)
-(* * Limit superior and inferior:                                             *)
-(*             sdrop u n := {u_k | k >= n}                                    *)
-(*                sups u := [sequence sup (sdrop u n)]_n                      *)
-(*                infs u := [sequence inf (sdrop u n)]_n                      *)
-(*         limn_{inf,sup} == limit inferior/superior for realType             *)
-(*               esups u := [sequence ereal_sup (sdrop u n)]_n                *)
-(*               einfs u := [sequence ereal_inf (sdrop u n)]_n                *)
-(*        limn_e{inf,sup} == limit inferior/superior for \bar R               *)
+(* * Limit superior and inferior for sequences:                               *)
+(*              sdrop u n := {u_k | k >= n}                                   *)
+(*                 sups u := [sequence sup (sdrop u n)]_n                     *)
+(*                 infs u := [sequence inf (sdrop u n)]_n                     *)
+(*     limn_sup, limn_inf == limit sup/inferior for a sequence of reals       *)
+(*                esups u := [sequence ereal_sup (sdrop u n)]_n               *)
+(*                einfs u := [sequence ereal_inf (sdrop u n)]_n               *)
+(* limn_esup u, limn_einf == limit sup/inferior for a sequence of             *)
+(*                           of extended reals                                *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -2579,8 +2580,36 @@ Qed.
 
 End esups_einfs.
 
-Definition limn_esup (R : realType) (u : (\bar R)^nat) := lim (esups u).
-Definition limn_einf (R : realType) (u : (\bar R)^nat) := lim (einfs u).
+Section limn_esup_einf.
+Context {R : realType}.
+Implicit Type (u : (\bar R)^nat).
+Local Open Scope ereal_scope.
+
+Definition limn_esup u := limf_esup u \oo.
+
+Definition limn_einf u := - limn_esup (\- u).
+
+Lemma limn_esup_lim u : limn_esup u = lim (esups u).
+Proof.
+apply/eqP; rewrite eq_le; apply/andP; split.
+  apply: lime_ge; first exact: is_cvg_esups.
+  near=> m; apply: ereal_inf_lb => /=.
+  by exists [set k | (m <= k)%N] => //=; exists m.
+apply: lb_ereal_inf => /= _ [A [r /= r0 rA] <-].
+apply: lime_le; first exact: is_cvg_esups.
+near=> m;   apply: le_ereal_sup => _ [n /= mn] <-.
+exists n => //; apply: rA => //=; apply: leq_trans mn.
+by near: m; exists r.
+Unshelve. all: by end_near. Qed.
+
+Lemma limn_einf_lim u : limn_einf u = lim (einfs u).
+Proof.
+rewrite /limn_einf limn_esup_lim esupsN -limeN//.
+  by under eq_fun do rewrite oppeK.
+by apply: is_cvgeN; exact: is_cvg_einfs.
+Qed.
+
+End limn_esup_einf.
 
 Section lim_esup_inf.
 Local Open Scope ereal_scope.
@@ -2590,7 +2619,8 @@ Implicit Types (u v : (\bar R)^nat) (l : \bar R).
 Lemma limn_einf_shift u l : l \is a fin_num ->
   limn_einf (fun x => l + u x) = l + limn_einf u.
 Proof.
-move=> lfin; apply/cvg_lim => //; apply: cvg_trans; last first.
+move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //.
+apply: cvg_trans; last first.
   by apply: (@cvgeD _ \oo _ _ (cst l) (einfs u) _ (lim (einfs u)));
     [exact: fin_num_adde_defr|exact: cvg_cst|exact: is_cvg_einfs].
 suff : einfs (fun n => l + u n) = (fun n => l + einfs u n) by move=> ->.
@@ -2611,25 +2641,22 @@ move=> supul ul; have usupu n : l <= u n <= esups u n.
 suff : esups u --> l.
   by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; [exact: nearW|exact: cvg_cst].
 apply/cvg_closeP; split; first exact: is_cvg_esups.
-rewrite closeE//; apply/eqP; rewrite eq_le supul.
+rewrite closeE//; apply/eqP.
+rewrite eq_le -[X in X <= _ <= _]limn_esup_lim supul/=.
 apply: (lime_ge (@is_cvg_esups _ _)); apply: nearW => m.
 have /le_trans : l <= einfs u m by apply: lb_ereal_inf => _ [p /= pm] <-.
 by apply; exact: einfs_le_esups.
 Qed.
 
 Lemma limn_einfN u : limn_einf (-%E \o u) = - limn_esup u.
-Proof.
-by rewrite /limn_einf einfsN /limn_esup limeN //; exact/is_cvg_esups.
-Qed.
+Proof. by rewrite /limn_esup -limf_einfN. Qed.
 
 Lemma limn_esupN u : limn_esup (-%E \o u) = - limn_einf u.
-Proof.
-apply/eqP; rewrite -eqe_oppLR -limn_einfN /=.
-by rewrite (_ : _ \o _ = u) // funeqE => n /=; rewrite oppeK.
-Qed.
+Proof. by rewrite /limn_einf oppeK. Qed.
 
 Lemma limn_einf_sup u : limn_einf u <= limn_esup u.
 Proof.
+rewrite limn_esup_lim limn_einf_lim.
 apply: lee_lim; [exact/is_cvg_einfs|exact/is_cvg_esups|].
 by apply: nearW; exact: einfs_le_esups.
 Qed.
@@ -2639,7 +2666,7 @@ Lemma cvgNy_limn_einf_sup u : u --> -oo ->
 Proof.
 move=> uoo; suff: limn_esup u = -oo.
   by move=> {}uoo; split => //; apply/eqP; rewrite -leeNy_eq -uoo limn_einf_sup.
-apply: cvg_lim => //=. apply/cvgeNyPle => M.
+rewrite limn_esup_lim; apply: cvg_lim => //=; apply/cvgeNyPle => M.
 have /cvgeNyPle/(_ M)[m _ uM] := uoo.
 near=> n; apply: ub_ereal_sup => _ [k /= nk <-].
 by apply: uM => /=; rewrite (leq_trans _ nk)//; near: n; exists m.
@@ -2648,13 +2675,14 @@ Unshelve. all: by end_near. Qed.
 Lemma cvgNy_einfs u : u --> -oo -> einfs u --> -oo.
 Proof.
 move=> /cvgNy_limn_einf_sup[uoo _].
-by apply/cvg_closeP; split; [exact: is_cvg_einfs|rewrite closeE].
+apply/cvg_closeP; split; [exact: is_cvg_einfs|rewrite closeE//].
+by rewrite -limn_einf_lim.
 Qed.
 
 Lemma cvgNy_esups u : u --> -oo -> esups u --> -oo.
 Proof.
-move=> /cvgNy_limn_einf_sup[_ uoo].
-by apply/cvg_closeP; split; [exact: is_cvg_esups|rewrite closeE].
+move=> /cvgNy_limn_einf_sup[_ uoo]; apply/cvg_closeP.
+by split; [exact: is_cvg_esups|rewrite closeE// -limn_esup_lim].
 Qed.
 
 Lemma cvgy_einfs u : u --> +oo -> einfs u --> +oo.
@@ -2700,7 +2728,9 @@ Qed.
 
 Lemma cvg_limn_einf_sup u l : u --> l -> (limn_einf u = l) * (limn_esup u = l).
 Proof.
-by move=> ul; split; apply/cvg_lim => //; [apply/cvg_einfs|apply/cvg_esups].
+move=> ul; rewrite limn_esup_lim limn_einf_lim; split.
+- by apply/cvg_lim => //; exact/cvg_einfs.
+- by apply/cvg_lim => //; exact/cvg_esups.
 Qed.
 
 Lemma is_cvg_limn_einfE u : cvg u -> limn_einf u = lim u.
diff --git a/theories/topology.v b/theories/topology.v
index 15a804186..b762064ab 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2611,6 +2611,10 @@ Definition dnbhs {T : topologicalType} (x : T) :=
   within (fun y => y != x) (nbhs x).
 Notation "x ^'" := (dnbhs x) : classical_set_scope.
 
+Lemma nbhs_dnbhs_neq {T : topologicalType} (p : T) :
+  \forall x \near nbhs p^', x != p.
+Proof. exact: withinT. Qed.
+
 Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x.
 Proof.
 rewrite predeqE => A; split=> [x_A|[x_A Ax]].
@@ -5148,6 +5152,13 @@ Lemma near_ball (y : M) (eps : {posnum R}) :
    \forall y' \near y, ball y eps%:num y'.
 Proof. exact: nbhsx_ballx. Qed.
 
+Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a).
+Proof.
+move: e => _/posnumP[e]; rewrite /dnbhs /within; near=> r => ra.
+split => //=; last exact/eqP.
+by near: r; rewrite near_simpl; exact: near_ball.
+Unshelve. all: by end_near. Qed.
+
 Lemma fcvg_ballP {F} {FF : Filter F} (y : M) :
   F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'.
 Proof. by rewrite -filter_fromP !nbhs_simpl /=. Qed.