diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v
index 85663cf85..2efb45db6 100644
--- a/theories/altreals/distr.v
+++ b/theories/altreals/distr.v
@@ -1220,7 +1220,7 @@ set c1 : R := _ / _; set c2 : R := _ / _; have eqc2: c2 = 1 - c1.
 set c := (li + l j); pose z := (c * c1 * f xi + c * c2 * f (x j)).
 apply/(@le_trans _ _ z); last by rewrite /z ![_*(_/_)]mulrC !mulfVK.
 rewrite {}/z -![c * _ * _]mulrA -mulrDr ler_wpmul2l ?addr_ge0 //.
-rewrite eqc2 cvx_f // divr_ge0 ?addr_ge0 //=.
+rewrite eqc2 cvx_f // ?lee_ninfty ?lee_pinfty // divr_ge0 ?addr_ge0 //=.
 by rewrite ler_pdivr_mulr ?mul1r ?ler_addl ?ltr_paddl.
 Qed.
 End Jensen.
diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v
index 3cced9164..9805b15c7 100644
--- a/theories/altreals/realseq.v
+++ b/theories/altreals/realseq.v
@@ -75,14 +75,14 @@ Qed.
 Lemma nbh_pinfW (P : forall x, nbh x -> Prop) :
   (forall M, P _ (@NPInf R M)) -> forall (v : nbh +oo), P _ v.
 Proof.
-move=> ih ; move: {-2}+oo (erefl (@ERPInf R)).
+move=> ih; move: {-2}+oo%E (erefl (@ERPInf R)).
 by move=> e eE v; case: v eE => // c' e' h [->].
 Qed.
 
 Lemma nbh_ninfW (P : forall x, nbh x -> Prop) :
   (forall M, P _ (@NNInf R M)) -> forall (v : nbh -oo), P _ v.
 Proof.
-move=> ih ; move: {-2}-oo (erefl (@ERNInf R)).
+move=> ih ; move: {-2}-oo%E (erefl (@ERNInf R)).
 by move=> e eE v; case: v eE => // c' e' h [->].
 Qed.
 End NbhElim.
@@ -386,7 +386,8 @@ Lemma ncvg_gt (u : nat -> R) (l1 l2 : {ereal R}) :
     exists K, forall n, (K <= n)%N -> (l1 < (u n)%:E)%E.
 Proof.
 case: l1 l2 => [l1||] [l2||] //=; first last.
-+ by move=> _ _; exists 0%N. + by move=> _ _; exists 0%N.
++ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
++ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
 + by move=> _ /(_ (NPInf l1)) [K cv]; exists K => n /cv.
 move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
 case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
@@ -439,7 +440,7 @@ move=> p; rewrite -[xchooseb _](ncvg_uniq cv_u_l) //.
 by apply/asboolP/(xchoosebP p).
 Qed.
 
-Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo.
+Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo%E.
 Proof.
 move=> h; rewrite /nlim; case: {-}_ / idP => // p.
 by case: h; case/existsbP: p => l /asboolP; exists l.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index 837ad558d..5836c3c9b 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -174,10 +174,11 @@ Proof.
 move=> mono_u; pose E := [pred x | `[exists n, x == u n]].
 have nzE: nonempty E by exists (u 0%N); apply/imsetbP; exists 0%N.
 case/boolP: `[< has_sup E >] => /asboolP; last first.
-  move/has_supPn=> -/(_ nzE) h; exists +oo => //; elim/nbh_pinfW => M /=.
+  move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=.
   case/(_ M): h=> x /imsetbP[K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
   by apply/(lt_le_trans lt_MuK)/mono_u.
-move=> supE; exists (sup E)%:E => //; elim/nbh_finW=>e /= gt0_e.
+move=> supE; exists (sup E)%:E => //; first exact: lte_ninfty.
+elim/nbh_finW=>e /= gt0_e.
 case: (sup_adherent supE gt0_e)=> x /imsetbP[K ->] lt_uK.
 exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
   by apply/sup_upper_bound/imsetbP=> //; exists n.
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index 1b445bc06..8cf0a56b5 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
-From mathcomp Require Import ssralg matrix.
+From mathcomp Require Import fintype bigop ssralg matrix.
 Require Import boolp.
 
 (******************************************************************************)
@@ -349,6 +349,14 @@ Qed.
 Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z.
 Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed.
 
+Lemma subsetI_neq0 T (A B C D : set T) :
+  A `<=` B -> C `<=` D -> A `&` C !=set0 -> B `&` D !=set0.
+Proof. by move=> AB CD [x [/AB Bx /CD Dx]]; exists x. Qed.
+
+Lemma subsetI_eq0 T (A B C D : set T) :
+  A `<=` B -> C `<=` D -> B `&` D = set0 -> A `&` C = set0.
+Proof. by move=> AB /(subsetI_neq0 AB); rewrite -!set0P => /contra_eq. Qed.
+
 Lemma setD_eq0 A (X Y : set A) : (X `\` Y = set0) = (X `<=` Y).
 Proof.
 rewrite propeqE; split=> [XDY0 a|sXY].
@@ -371,6 +379,9 @@ Proof. by rewrite predeqE => ?; split=> [[]|[]]. Qed.
 Lemma setIT {A} (X : set A) : X `&` setT = X.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
+Lemma setTI {A} (X : set A) : setT `&` X = X.
+Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
+
 Lemma setI0 {A} (X : set A) : X `&` set0 = set0.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
@@ -378,7 +389,7 @@ Lemma set0I A (Y : set A) : set0 `&` Y = set0.
 Proof. by rewrite setIC setI0. Qed.
 
 Lemma setICl {A} (X : set A) : ~` X `&` X = set0.
-Proof. by rewrite predeqE => ?; split => // -[]. Qed.
+Proof. by rewrite predeqE => ?; split => // -[]. Qed.
 
 Lemma setIA {A} (X Y Z : set A) : X `&` (Y `&` Z) = X `&` Y `&` Z.
 Proof. by rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.
@@ -403,10 +414,16 @@ Lemma setUC A : commutative (@setU A).
 Proof. move=> p q; rewrite /setU predeqE => a; tauto. Qed.
 
 Lemma set0U T (X : set T) : set0 `|` X = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|right]. Qed.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU0 T (X : set T) : X `|` set0 = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|left]. Qed.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setTU T (X : set T) : setT `|` X = setT.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setUT T (X : set T) : X `|` setT = setT.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU_eq0 T (X Y : set T) : (X `|` Y = set0) = ((X = set0) /\ (Y = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.
@@ -425,6 +442,26 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
 by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
 Qed.
 
+Lemma setIDl T : left_distributive (@setI T) (@setU T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt|Yt] Zt]; [left|right].
+by move=> [[Xt Zt]|[Yt Zt]]; split => //; [left|right].
+Qed.
+
+Lemma setIDr T : right_distributive (@setI T) (@setU T).
+Proof. by move=> X Y Z; rewrite ![X `&` _]setIC setIDl. Qed.
+
+Lemma setUDl T : left_distributive (@setU T) (@setI T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt Yt]|Zt]; split; by [left|right].
+by move=> [[Xt|Zt] [Yt|Zt']]; by [left|right].
+Qed.
+
+Lemma setUDr T : right_distributive (@setU T) (@setI T).
+Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.
+
 Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := all (is_subset1 \o f).
 Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
@@ -476,6 +513,39 @@ Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a
   is_subset1 (f a) -> forall b, f a b ->  fun_of_rel f0 f a = b.
 Proof. by move=> fa_prop b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.
 
+Section SetMonoids.
+Variable (T : Type).
+
+Import Monoid.
+Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
+Canonical setU_comoid := ComLaw (@setUC T).
+Canonical setU_mul_monoid := MulLaw (@setTU T) (@setUT T).
+Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
+Canonical setI_comoid := ComLaw (@setIC T).
+Canonical setI_mul_monoid := MulLaw (@set0I T) (@setI0 T).
+Canonical setU_add_monoid := AddLaw (@setUDl T) (@setUDr T).
+Canonical setI_add_monoid := AddLaw (@setIDl T) (@setIDr T).
+
+End SetMonoids.
+
+Lemma bigcup_ord T n (A : nat -> set T) :
+ \big[setU/set0]_(i < n) A i = \bigcup_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE; split => -[].
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0|[i AS]]; [exists 0%N|exists i.+1].
+by move=> [[|i] Ai]; [left|right; exists i].
+Qed.
+
+Lemma bigcap_ord T n (A : nat -> set T) :
+ \big[setI/setT]_(i < n) A i = \bigcap_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE.
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0 AS] [|i]// /AS.
+by move=> AP; split => [|i i_lt]; apply: AP.
+Qed.
+
 Module Pointed.
 
 Definition point_of (T : Type) := T.
diff --git a/theories/derive.v b/theories/derive.v
index 6dda95fea..d33d79b2e 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -108,10 +108,10 @@ Lemma diff_locallyxP (x : V) (f : V -> W) :
 Proof.
 split=> [dxf|[dfc dxf]].
   split => //; apply: eqaddoEx => h; have /diffE -> := dxf.
-  rewrite lim_id addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
+  rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
   by congr ('o); rewrite funeqE => k /=; rewrite addrK.
 apply/diffP; split=> //; apply: eqaddoEx; move=> y.
-rewrite lim_id -[in LHS](subrK x y) dxf; congr (_ + _).
+rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _).
 rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x).
 by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0.
 Qed.
@@ -297,7 +297,7 @@ rewrite /derive => /diff_locally -> /=; set k := 'o _.
 evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
   rewrite funeqE=> h; rewrite !scalerDr scalerN /cst /=.
   by rewrite addrC !addrA addNr add0r linearZ /= scalerA /g.
-apply: cvg_map_lim.
+apply: cvg_map_lim => //.
 pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
 pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
 rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
@@ -525,7 +525,7 @@ suff /diff_locally /hdf -> : differentiable f x.
 apply/diffP; apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\
   forall y, f y = f (lim x) + df (y - lim x) +o_(y \near x) (y - lim x))).
 exists df; split=> //; apply: eqaddoEx => z.
-rewrite (hdf _ dxf) !addrA lim_id /(_ \o _) /= subrK [f _ + _]addrC addrK.
+rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK.
 rewrite -addrA -[LHS]addr0; congr (_ + _).
 apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
 by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
@@ -1376,7 +1376,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_right_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_right _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
 by exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
 Qed.
 
@@ -1386,7 +1386,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_left_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_left _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
 exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _].
 by apply: xe_A => //; rewrite eq_sym.
 Qed.
@@ -1411,7 +1411,7 @@ Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
 Proof.
 move=> fle0 fcv; rewrite -oppr_ge0.
 have limopp : - lim (f @ F) = lim (- f @ F).
-  by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgN.
+  by apply: Logic.eq_sym; apply: cvg_map_lim => //; apply: cvgN.
 rewrite limopp; apply: le0r_cvg_map; last by rewrite -limopp; apply: cvgN.
 by move: fle0; apply: filterS => x; rewrite oppr_ge0.
 Qed.
@@ -1423,7 +1423,7 @@ Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (F
 Proof.
 move=> lefg fcv gcv; rewrite -subr_ge0.
 have eqlim : lim (g @ F) - lim (f @ F) = lim ((g - f) @ F).
-  by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgD => //; apply: cvgN.
+  by apply/esym; apply: cvg_map_lim => //; apply: cvgD => //; apply: cvgN.
 rewrite eqlim; apply: le0r_cvg_map; last first.
   by rewrite /(cvg _) -eqlim /=; apply: cvgD => //; apply: cvgN.
 by move: lefg; apply: filterS => x; rewrite subr_ge0.
diff --git a/theories/ereal.v b/theories/ereal.v
index bb5efeaad..6bc6d102f 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -29,9 +29,9 @@ End ExtendedReals.
 (* TODO: the following notations should have scopes. *)
 
 (*Notation "\+inf" := (@ERPInf _).*)
-Notation "+oo" := (@ERPInf _).
+Notation "+oo" := (@ERPInf _) : ereal_scope.
 (*Notation "\-inf" := (@ERNInf _).*)
-Notation "-oo" := (@ERNInf _).
+Notation "-oo" := (@ERNInf _) : ereal_scope.
 Notation "x %:E" := (@ERFin _ x) (at level 2, format "x %:E").
 
 Notation "{ 'ereal' R }" := (er R) (format "{ 'ereal'  R }").
@@ -39,6 +39,8 @@ Notation "{ 'ereal' R }" := (er R) (format "{ 'ereal'  R }").
 Bind    Scope ereal_scope with er.
 Delimit Scope ereal_scope with E.
 
+Local Open Scope ereal_scope.
+
 Section EqEReal.
 Variable (R : eqType).
 
@@ -65,7 +67,7 @@ Variable (R : choiceType).
 
 Definition code (x : {ereal R}) :=
   match x with
-  | x%:E  => GenTree.Node 0 [:: GenTree.Leaf x]
+  | x%:E => GenTree.Node 0 [:: GenTree.Leaf x]
   | +oo => GenTree.Node 1 [::]
   | -oo => GenTree.Node 2 [::]
   end.
@@ -99,19 +101,19 @@ Implicit Types (x y : {ereal R}).
 
 Definition le_ereal x1 x2 :=
   match x1, x2 with
-  | -oo, _ | _, +oo => true
-  | +oo, _ | _, -oo => false
-
+  | -oo, x%:E | x%:E, +oo => x \is Num.real
   | x1%:E, x2%:E => x1 <= x2
+  | -oo, _    | _, +oo => true
+  | +oo, _    | _, -oo => false
   end.
 
 Definition lt_ereal x1 x2 :=
   match x1, x2 with
-  | -oo, -oo | +oo, +oo => false
-  | -oo, _   | _  , +oo => true
-  | +oo, _   | _  , -oo => false
-
+  | -oo, x%:E | x%:E, +oo => x \is Num.real
   | x1%:E, x2%:E => x1 < x2
+  | -oo, -oo  | +oo, +oo => false
+  | +oo, _    | _  , -oo => false
+  | -oo, _  => true
   end.
 
 Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.
@@ -121,10 +123,14 @@ Lemma le_refl_ereal : reflexive le_ereal.
 Proof. by case => /=. Qed.
 
 Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
-Proof. by case=> [?||][?||] //= /le_anti ->. Qed.
+Proof. by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.
 
 Lemma le_trans_ereal : ssrbool.transitive le_ereal.
-Proof. by case=> [?||][?||][?||] //=; exact: le_trans. Qed.
+Proof.
+case=> [?||][?||][?||] //=; rewrite -?comparabler0; first exact: le_trans.
+  by move=> /le_comparable cmp /(comparabler_trans cmp).
+by move=> cmp /ge_comparable /comparabler_trans; apply.
+Qed.
 
 Fact ereal_display : unit. Proof. by []. Qed.
 
@@ -151,12 +157,24 @@ Notation "x < y <= z"  := ((lte x y) && (lee y z)) : ereal_scope.
 Notation "x <= y < z"  := ((lee x y) && (lte y z)) : ereal_scope.
 Notation "x < y < z"   := ((lte x y) && (lte y z)) : ereal_scope.
 
-Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y).
+Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y)%O.
 Proof. by []. Qed.
 
-Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y).
+Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y)%O.
 Proof. by []. Qed.
 
+Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
+Proof. exact: num_real. Qed.
+
+Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
+Proof. case: x => //= r; exact: num_real. Qed.
+
+Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
+Proof. exact: num_real. Qed.
+
+Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
+Proof. case: x => //= r; exact: num_real. Qed.
+
 Section ERealOrder_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y : {ereal R}).
@@ -196,7 +214,10 @@ Lemma meetKU_ereal y x : max_ereal x (min_ereal x y) = x.
 Proof. by case: x y => [?||][?||] //=; rewrite (meetKU, joinxx). Qed.
 
 Lemma leEmeet_ereal x y : (x <= y)%E = (min_ereal x y == x).
-Proof. by case: x y => [x||][y||] //=; [exact: leEmeet | rewrite eqxx]. Qed.
+Proof.
+case: x y => [x||][y||] //=; rewrite ?eqxx ?lee_pinfty ?lee_ninfty //.
+exact: leEmeet.
+Qed.
 
 Lemma meetUl_ereal : left_distributive min_ereal max_ereal.
 Proof.
@@ -204,14 +225,13 @@ by case=> [?||][?||][?||] //=; rewrite ?(meetUl, meetUK, meetKUC, joinxx).
 Qed.
 
 Lemma minE_ereal x y : min_ereal x y = if le_ereal x y then x else y.
-Proof. by case: x y => [?||][?||] //=; case: leP. Qed.
+Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: leP. Qed.
 
 Lemma maxE_ereal x y : max_ereal x y = if le_ereal y x then x else y.
-Proof.
-Proof. by case: x y => [?||][?||] //=; case: ltP. Qed.
+Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: ltP. Qed.
 
 Lemma le_total_ereal : total (@le_ereal R).
-Proof. by case=> [?||][?||] //=; exact: le_total. Qed.
+Proof. by case=> [?||][?||] //=; rewrite ?num_real //; exact: le_total. Qed.
 
 Definition ereal_latticeMixin :=
   LatticeMixin min_erealC max_erealC min_erealA max_erealA
diff --git a/theories/landau.v b/theories/landau.v
index 024e21974..86e01fdea 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -1139,7 +1139,7 @@ Hypothesis (normm_s : forall k x, `|s k x| = `|k| * `|x|).
 (* - locally lipschitz => continuous at a point *)
 (* - lipschitz => uniformly continous *)
 
-Local Notation "'+oo'" := (@ERPInf R).
+Local Notation "'+oo'" := (@pinfty_locally R).
 
 Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.op s_law}) :
   (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 974180a10..b107870e9 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -419,34 +419,254 @@ Proof. exact: Proper_locally'_numFieldType. Qed.
 
 (** * Some Topology on [Rbar] *)
 
+Canonical ereal_pointed (R : numDomainType) := PointedType {ereal R} (+oo%E).
+
 Section ereal_locally.
 Context {R : numFieldType}.
 Let R_topologicalType := [topologicalType of R^o].
-Definition ereal_locally' (a : {ereal R}) (P : R -> Prop) :=
+Local Open Scope ereal_scope.
+Definition ereal_locally' (a : {ereal R}) (P : {ereal R} -> Prop) : Prop :=
   match a with
-    | a%:E => @locally' R_topologicalType a P
-    | +oo => exists M, M \is Num.real /\ forall x, M < x -> P x
-    | -oo => exists M, M \is Num.real /\ forall x, x < M -> P x
+    | a%:E => @locally' R_topologicalType a (fun x => P x%:E)
+    | +oo => exists M, M \is Num.real /\ forall x, (M%:E < x)%E -> P x
+    | -oo => exists M, M \is Num.real /\ forall x, (x < M%:E)%E -> P x
   end.
-Definition ereal_locally (a : {ereal R}) (P : R -> Prop) :=
+Definition ereal_locally (a : {ereal R}) (P : {ereal R} -> Prop) : Prop :=
   match a with
-    | a%:E => @locally _ R_topologicalType a P
-    | +oo => exists M, M \is Num.real /\ forall x, M < x -> P x
-    | -oo => exists M, M \is Num.real /\ forall x, x < M -> P x
+    | a%:E => @locally _ R_topologicalType a (fun x => P x%:E)
+    | +oo => exists M, M \is Num.real /\ forall x, (M%:E < x)%E -> P x
+    | -oo => exists M, M \is Num.real /\ forall x, (x < M%:E)%E -> P x
   end.
-
-(*Canonical Rbar_choiceType := ChoiceType Rbar gen_choiceMixin.*)
-Canonical ereal_pointed := PointedType {ereal R} (+oo).
-Canonical ereal_filter := FilteredType R {ereal R} (ereal_locally).
+Canonical ereal_ereal_filter := FilteredType {ereal R} {ereal R} (ereal_locally).
 End ereal_locally.
 
-Section ereal_locally.
+Section ereal_locally_instances.
 Context {R : numFieldType}.
 Let R_topologicalType := [topologicalType of R^o].
 
 Global Instance ereal_locally'_filter :
   forall x : {ereal R}, ProperFilter (ereal_locally' x).
 Proof.
+case=> [x||].
+- case: (Proper_locally'_numFieldType x) => x0 [//= xT xI xS].
+  apply Build_ProperFilter' => //=; apply Build_Filter => //=.
+  move=> P Q lP lQ; exact: xI.
+  by move=> P Q PQ /xS; apply => y /PQ.
+- apply Build_ProperFilter.
+    move=> P [x [xr xP]]; exists (x + 1)%:E; apply xP => /=.
+    by rewrite lte_fin ltr_addl.
+  split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
+  + by exists 0; rewrite real0.
+  + have [/eqP MP0|MP0] := boolP (MP == 0).
+      have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+        by exists 0; rewrite real0; split => // x x0; split;
+        [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
+      exists `|MQ|; rewrite realE normr_ge0; split => // x Hx; split.
+        by apply gtMP; rewrite (le_lt_trans _ Hx) // MP0 lee_fin.
+      by apply gtMQ; rewrite (le_lt_trans _ Hx) // lee_fin real_ler_normr // lexx.
+    have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+      exists `|MP|; rewrite realE normr_ge0; split => // x MPx; split.
+      by apply gtMP; rewrite (le_lt_trans _ MPx) // lee_fin real_ler_normr // lexx.
+      by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
+    have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
+    have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
+    exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
+    rewrite realE /= posnum_ge0 /=; split => //.
+    case=> [r| |//].
+    * rewrite lte_fin pos_ltUx /= => /andP[MPx MQx]; split.
+      by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx) // real_ler_normr // lexx.
+      by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx) // real_ler_normr // lexx.
+    * by move=> _; split; [apply/gtMP | apply/gtMQ].
+  + by exists M; split => // ? /gtM /sPQ.
+- apply Build_ProperFilter.
+  + move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
+    by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0.
+  + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
+    * by exists 0; rewrite real0.
+    * have [/eqP MP0|MP0] := boolP (MP == 0).
+        have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+          by exists 0; rewrite real0; split => // x x0; split;
+          [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
+        exists (- `|MQ|); rewrite realN realE normr_ge0; split => // x xMQ; split.
+          by apply ltMP; rewrite (lt_le_trans xMQ) // lee_fin MP0 ler_oppl oppr0.
+       apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
+       by rewrite real_ler_normr ?realN // lexx.
+    * have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+        exists (- `|MP|); rewrite realN realE normr_ge0; split => // x MPx; split.
+          apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
+          by rewrite real_ler_normr ?realN // lexx.
+        by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
+      have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
+      have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
+      exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
+      rewrite realN realE /= posnum_ge0 /=; split => //.
+      case=> [r|//|].
+      - rewrite lte_fin ltr_oppr pos_ltUx => /andP[].
+        rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
+          apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN.
+          by rewrite real_ler_normr ?realN // lexx.
+        apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= ler_oppl -normrN.
+        by rewrite real_ler_normr ?realN // lexx.
+      - by move=> _; split; [apply/ltMP | apply/ltMQ].
+    * by exists M; split => // x /ltM /sPQ.
+Qed.
+Typeclasses Opaque ereal_locally'.
+
+Global Instance ereal_locally_filter :
+  forall x, ProperFilter (@ereal_locally R x).
+Proof.
+case=> [x| |].
+- case: (ereal_locally'_filter x%:E) => x0 [//=nxT xI xS].
+  apply Build_ProperFilter => //=.
+  by move=> P [r r0 xr]; exists x%:E; apply xr => //=; rewrite subrr normr0.
+  apply Build_Filter => //=.
+  by rewrite locallyE'.
+  move=> P Q.
+  rewrite !locallyE' => -[xP axP] [xQ axQ]; split => //=.
+  exact: xI.
+  move=> P Q PQ; rewrite !locallyE' => -[xP axP]; split => //=.
+  apply (xS P) => //=.
+  exact: PQ.
+exact: (ereal_locally'_filter +oo).
+exact: (ereal_locally'_filter -oo).
+Qed.
+Typeclasses Opaque ereal_locally.
+
+End ereal_locally_instances.
+
+Section ereal_topologicalType.
+Variable R : realFieldType.
+
+Lemma ereal_loc_singleton (p : {ereal R}) (A : set {ereal R}) :
+  ereal_locally p A -> A p.
+Proof.
+move: p => -[p | [M [Mreal MA]] | [M [Mreal MA]]] /=; [|exact: MA | exact: MA].
+move/locallyP; rewrite locally_E => -[_/posnumP[e]]; apply; exact/ballxx.
+Qed.
+
+Lemma ereal_loc_loc (p : {ereal R}) (A : set {ereal R}) :
+  ereal_locally p A -> ereal_locally p (ereal_locally^~ A).
+Proof.
+move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
+- move/locallyP; rewrite locally_E => -[_/posnumP[e]] ballA.
+  apply/locallyP; rewrite locally_E; exists (e%:num / 2) => //= r per.
+  apply/locallyP; rewrite locally_E; exists (e%:num / 2) => //= x rex.
+  apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym.
+- exists (M + 1); split; first by rewrite realD // real1.
+  move=> -[x| _ |] //=.
+    rewrite lte_fin => M'x /=.
+    apply/locallyP; rewrite locally_E; exists 1 => //= y x1y.
+    apply MA; rewrite lte_fin.
+    rewrite addrC -ltr_subr_addl in M'x.
+    rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
+      rewrite ltr_subr_addr in M'x.
+      rewrite -comparabler0 (@comparabler_trans _ (M + 1)) //.
+        by rewrite /Order.comparable (ltW M'x) orbT.
+      by rewrite comparabler0 realD // real1.
+    by rewrite num_real. (* where we really use realFieldType *)
+  by exists M.
+- exists (M - 1); split; first by rewrite realB // real1.
+  move=> -[x| _ |] //=.
+    rewrite lte_fin => M'x /=.
+    apply/locallyP; rewrite locally_E; exists 1 => //= y x1y.
+    apply MA; rewrite lte_fin.
+    rewrite ltr_subr_addl in M'x.
+    rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
+      by rewrite num_real. (* where we really use realFieldType *)
+    rewrite addrC -ltr_subr_addr in M'x.
+    rewrite -comparabler0 (@comparabler_trans _ (M - 1)) //.
+      by rewrite /Order.comparable (ltW M'x).
+    by rewrite comparabler0 realB // real1.
+  by exists M.
+Qed.
+
+Definition ereal_topologicalMixin : Topological.mixin_of (@ereal_locally R) :=
+  topologyOfFilterMixin _ ereal_loc_singleton ereal_loc_loc.
+Canonical ereal_topologicalType := TopologicalType _ ereal_topologicalMixin.
+
+End ereal_topologicalType.
+
+Definition pinfty_locally (R : numFieldType) : set (set R) :=
+  fun P => exists M, M \is Num.real /\ forall x, M < x -> P x.
+Arguments pinfty_locally R : clear implicits.
+Definition ninfty_locally (R : numFieldType) : set (set R) :=
+  fun P => exists M, M \is Num.real /\ forall x, x < M -> P x.
+Arguments ninfty_locally R : clear implicits.
+
+Notation "+oo" := (pinfty_locally _) : ring_scope.
+Notation "-oo" := (ninfty_locally _) : ring_scope.
+
+Section infty_locally_instances.
+Context {R : numFieldType}.
+Let R_topologicalType := [topologicalType of R^o].
+
+Global Instance proper_pinfty_locally : ProperFilter (pinfty_locally R).
+Proof.
+apply Build_ProperFilter.
+  by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltr_addl.
+split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
+- by exists 0; rewrite real0.
+- have [/eqP MP0|MP0] := boolP (MP == 0).
+    have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+      by exists 0; rewrite real0; split => // x x0; split;
+      [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
+    exists `|MQ|; rewrite realE normr_ge0; split => // x Hx; split.
+      by apply gtMP; rewrite (le_lt_trans _ Hx) // MP0.
+    by apply gtMQ; rewrite (le_lt_trans _ Hx) // real_ler_normr // lexx.
+  have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+    exists `|MP|; rewrite realE normr_ge0; split => // x MPx; split.
+    by apply gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
+    by apply gtMQ; rewrite (le_lt_trans _ MPx) // MQ0.
+  have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
+  have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
+  exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
+  rewrite realE /= posnum_ge0 /=; split => // x.
+  rewrite pos_ltUx /= => /andP[MPx MQx]; split.
+  by apply/gtMP; rewrite (le_lt_trans _ MPx) // real_ler_normr // lexx.
+  by apply/gtMQ; rewrite (le_lt_trans _ MQx) // real_ler_normr // lexx.
+- by exists M; split => // ? /gtM /sPQ.
+Defined.
+Typeclasses Opaque proper_pinfty_locally.
+
+Global Instance proper_ninfty_locally : ProperFilter (ninfty_locally R).
+Proof.
+apply Build_ProperFilter.
+- move=> P [M [Mr ltMP]]; exists (M - 1).
+  by apply: ltMP; rewrite gtr_addl oppr_lt0.
+- split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
+  + by exists 0; rewrite real0.
+  + have [/eqP MP0|MP0] := boolP (MP == 0).
+      have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+        by exists 0; rewrite real0; split => // x x0; split;
+        [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
+      exists (- `|MQ|); rewrite realN realE normr_ge0; split => // x xMQ; split.
+        by apply ltMP; rewrite (lt_le_trans xMQ) // MP0 ler_oppl oppr0.
+      apply ltMQ; rewrite (lt_le_trans xMQ) // ler_oppl -normrN.
+     by rewrite real_ler_normr ?realN // lexx.
+  + have [/eqP MQ0|MQ0] := boolP (MQ == 0).
+      exists (- `|MP|); rewrite realN realE normr_ge0; split => // x MPx; split.
+        apply ltMP; rewrite (lt_le_trans MPx) // ler_oppl -normrN.
+        by rewrite real_ler_normr ?realN // lexx.
+      by apply ltMQ; rewrite (lt_le_trans MPx) // MQ0 ler_oppl oppr0.
+    have {}MP0 : 0 < `|MP| by rewrite normr_gt0.
+    have {}MQ0 : 0 < `|MQ| by rewrite normr_gt0.
+    exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num).
+    rewrite realN realE /= posnum_ge0 /=; split => // x.
+    rewrite ltr_oppr pos_ltUx => /andP[].
+    rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
+      apply/ltMP; rewrite (lt_le_trans MPx) //= ler_oppl -normrN.
+      by rewrite real_ler_normr ?realN // lexx.
+    apply/ltMQ; rewrite (lt_le_trans MQx) //= ler_oppl -normrN.
+    by rewrite real_ler_normr ?realN // lexx.
+  + by exists M; split => // x /ltM /sPQ.
+Defined.
+Typeclasses Opaque proper_ninfty_locally.
+
+(*Global Instance ereal_locally'_filter :
+  forall x : {ereal R}, ProperFilter (ereal_locally' x).
+Proof.
 case=> [x||]; first exact: Proper_locally'_numFieldType.
 - apply Build_ProperFilter.
     by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltr_addl.
@@ -501,17 +721,17 @@ case=> [x||]; first exact: Proper_locally'_numFieldType.
       by rewrite real_ler_normr ?realN // lexx.
     * by exists M; split => // x /ltM /sPQ.
 Qed.
-Typeclasses Opaque ereal_locally'.
+Typeclasses Opaque ereal_locally'.*)
 
-Global Instance ereal_locally_filter :
+(*Global Instance ereal_locally_filter :
   forall x, ProperFilter (@ereal_locally R x).
 Proof.
 case=> [x||].
-by apply/(@locally_filter R_topologicalType).
+exact: ereal_locally_filter.
 exact: (ereal_locally'_filter +oo).
 exact: (ereal_locally'_filter -oo).
 Qed.
-Typeclasses Opaque ereal_locally.
+Typeclasses Opaque ereal_locally.*)
 
 Lemma near_pinfty_div2 (A : set R) :
   (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)).
@@ -527,7 +747,7 @@ Proof. by  exists c%:num; split => // ; rewrite realE posnum_ge0. Qed.
 Lemma locally_pinfty_ge (c : {posnum R}) : \forall x \near +oo, c%:num <= x.
 Proof. by exists c%:num; rewrite realE posnum_ge0; split => //; apply: ltW. Qed.
 
-End ereal_locally.
+End infty_locally_instances.
 
 Hint Extern 0 (is_true (0 < _)) => match goal with
   H : ?x \is_near (locally +oo) |- _ =>
@@ -714,35 +934,59 @@ Lemma cvg_norm {F : set (set V)} {FF : Filter F} (y : V) :
   F --> y -> forall eps, eps > 0 -> \forall y' \near F, `|y - y'| < eps.
 Proof. by move=> /cvg_normP. Qed.
 
-Lemma closeE (x y : V) : close x y = (x = y).
-Proof.
-rewrite propeqE; split => [cl_xy|->//]; have [//|neq_xy] := eqVneq x y.
-have dxy_gt0 : `|x - y| > 0.
-  by rewrite normr_gt0 subr_eq0.
-have dxy_ge0 := ltW dxy_gt0.
-have := cl_xy (PosNum dxy_gt0).
-by rewrite -ball_normE /= ltxx.
-Qed.
-
-Lemma eq_close (x y : V) : close x y -> x = y. by rewrite closeE. Qed.
-
 Lemma locally_norm_ball x (eps : {posnum R}) : locally_norm x (ball x eps%:num).
 Proof. rewrite locally_locally_norm; by apply: locally_ball. Qed.
 
-Lemma norm_close x y : close x y = (forall eps : {posnum R}, ball_norm x eps%:num y).
-Proof. by rewrite propeqE ball_normE. Qed.
-
 End NormedModule_numDomainType.
 Hint Resolve normr_ge0 : core.
 Arguments cvg_norm {_ _ F FF}.
 
 Section NormedModule_numFieldType.
 Variables (R : numFieldType) (V : normedModType R).
+Implicit Types (x y z : V).
 
 Local Notation ball_norm := (ball_ (@normr R V)).
 
 Local Notation locally_norm := (locally_ ball_norm).
 
+Lemma norm_hausdorff : hausdorff V.
+Proof.
+rewrite ball_hausdorff => a b ab.
+have ab2 : 0 < `|a - b| / 2 by apply divr_gt0 => //; rewrite normr_gt0 subr_eq0.
+set r := PosNum ab2; exists (r, r) => /=.
+apply/negPn/negP => /set0P[c] []; rewrite -ball_normE /ball_ => acr bcr.
+have r22 : r%:num * 2 = r%:num + r%:num by rewrite (_ : 2 = 1 + 1) // mulrDr mulr1.
+move: (ltr_add acr bcr); rewrite -r22 (distrC b c).
+move/(le_lt_trans (ler_dist_add c a b)).
+by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE.
+Qed.
+Hint Extern 0 (hausdorff _) => solve[apply: norm_hausdorff] : core.
+
+(* TODO: check if the following lemma are indeed useless *)
+(*       i.e. where the generic lemma is applied, *)
+(*            check that norm_hausdorff is not used in a hard way *)
+
+Lemma norm_closeE x y : close x y = (x = y). Proof. exact: closeE. Qed.
+Lemma norm_close_eq x y : close x y -> x = y. Proof. exact: close_eq. Qed.
+
+Lemma norm_cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : V | F --> x].
+Proof. exact: cvg_unique. Qed.
+
+Lemma norm_cvg_eq x y : x --> y -> x = y. Proof. exact: cvg_eq. Qed.
+Lemma norm_lim_id x : lim x = x. Proof. exact: lim_id. Qed.
+
+Lemma norm_cvg_lim {F} {FF : ProperFilter F} (l : V) : F --> l -> lim F = l.
+Proof. exact: cvg_lim. Qed.
+
+Lemma norm_cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set V) :
+  {near F, is_fun f} -> is_subset1 [set x : V | f `@ F --> x].
+Proof. exact: cvgi_unique. Qed.
+
+Lemma norm_cvgi_map_lim {U} {F} {FF : ProperFilter F} (f : U -> V -> Prop) (l : V) :
+  F (fun x : U => is_subset1 (f x)) ->
+  f `@ F --> l -> lim (f `@ F) = l.
+Proof. exact: cvgi_map_lim. Qed.
+
 Lemma distm_lt_split (z x y : V) (e : R) :
   `|x - z| < e / 2 -> `|z - y| < e / 2 -> `|x - y| < e.
 Proof. by have := @ball_split _ _ z x y e; rewrite -ball_normE. Qed.
@@ -767,28 +1011,6 @@ Proof.
 by move=> xlt ylt; rewrite -[y]opprK (@distm_lt_split 0) ?subr0 ?opprK ?add0r.
 Qed.
 
-Lemma cvg_unique {F} {FF : ProperFilter F} :
-  is_subset1 [set x : V | F --> x].
-Proof. by move=> Fx Fy; rewrite -closeE; apply: cvg_close. Qed.
-
-Lemma locally_cvg_unique (x y : V) : x --> y -> x = y.
-Proof. by rewrite -closeE; apply: cvg_close. Qed.
-
-Lemma lim_id (x : V) : lim x = x.
-Proof. by symmetry; apply: locally_cvg_unique; apply/cvg_ex; exists x. Qed.
-
-Lemma cvg_lim {F} {FF : ProperFilter F} (l : V) :
-  F --> l -> lim F = l.
-Proof. by move=> Fl; have Fcv := cvgP Fl; apply: (@cvg_unique F). Qed.
-
-Lemma cvg_map_lim {T : Type} {F} {FF : ProperFilter F} (f : T -> V) (l : V) :
-  f @ F --> l -> lim (f @ F) = l.
-Proof. exact: cvg_lim. Qed.
-
-Lemma cvgi_unique {T : Type} {F} {FF : ProperFilter F} (f : T -> set V) :
-  {near F, is_fun f} -> is_subset1 [set x : V | f `@ F --> x].
-Proof. by move=> ffun fx fy; rewrite -closeE; apply: cvgi_close. Qed.
-
 Lemma cvg_normW {F : set (set V)} {FF : Filter F} (y : V) :
   (forall eps, 0 < eps -> \forall y' \near F, `|y - y'| <= eps) ->
   F --> y.
@@ -797,14 +1019,6 @@ move=> cv; apply/cvg_normP => _/posnumP[e]; near=> x.
 by apply: normm_leW => //; near: x; apply: cv.
 Grab Existential Variables. all: end_near. Qed.
 
-Lemma cvgi_map_lim {T} {F} {FF : ProperFilter F} (f : T -> V -> Prop) (l : V) :
-  F (fun x : T => is_subset1 (f x)) ->
-  f `@ F --> l -> lim (f `@ F) = l.
-Proof.
-move=> f_prop f_l; apply: get_unique => // l' f_l'.
-exact: cvgi_unique _ f_l' f_l.
-Qed.
-
 Lemma cvg_bounded_real {F : set (set V)} {FF : Filter F} (y : V) :
   F --> y ->
   \forall M \near +oo, M \is Num.real /\ \forall y' \near F, `|y'| < M.
@@ -827,6 +1041,7 @@ Proof. move/cvg_bounded_real; by apply: filterS => x []. Qed.
 
 End NormedModule_numFieldType.
 Arguments cvg_bounded {_ _ F FF}.
+Hint Extern 0 (hausdorff _) => solve[apply: norm_hausdorff] : core.
 
 Module Export LocallyNorm.
 Definition locally_simpl :=
@@ -846,20 +1061,6 @@ rewrite (subr_trans z) (le_trans (ler_norm_add _ _) _)// ltW //.
 by rewrite (splitr e%:num) (distrC z); apply: ltr_add.
 Qed.
 
-Lemma normedModType_hausdorff (R : realFieldType) (V : normedModType R) :
-  hausdorff V.
-Proof.
-move=> p q clp_q; apply/subr0_eq/normr0_eq0/Rhausdorff => A B pq_A.
-rewrite -(@normr0 _ V) -(subrr p) => pp_B.
-suff loc_preim r C : @locally _ [filteredType R of R^o] `|p - r| C ->
-    locally r ((fun r => `|p - r|) @^-1` C).
-  have [r []] := clp_q _ _ (loc_preim _ _ pp_B) (loc_preim _ _ pq_A).
-  by exists `|p - r|.
-move=> [e egt0 pre_C]; apply: locally_le_locally_norm; exists e => // s re_s.
-apply: pre_C; apply: le_lt_trans (ler_dist_dist _ _) _.
-by rewrite opprB addrC -subr_trans distrC.
-Qed.
-
 End hausdorff.
 
 Module Export NearNorm.
@@ -1542,7 +1743,7 @@ Qed.
 
 Section NVS_continuity1.
 Context {K : numFieldType} {V : normedModType K}.
-Local Notation "'+oo'" := (@ERPInf K).
+Local Notation "'+oo'" := (pinfty_locally K).
 
 Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
 Proof.
@@ -1896,7 +2097,7 @@ End TODO_add_to_ssrnum.
 
 Section cvg_seq_bounded.
 Context {K : numFieldType}.
-Local Notation "'+oo'" := (@ERPInf K).
+Local Notation "'+oo'" := (@pinfty_locally K).
 
 (* TODO: simplify using extremumP when PR merged in mathcomp *)
 Lemma cvg_seq_bounded {V : normedModType K} (a : nat -> V) :
@@ -2199,10 +2400,10 @@ move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
     by rewrite -subr_gt0 opprD addrA {1}[b - x]splitr addrK divr_gt0 ?subr_gt0.
   by rewrite -subr_gt0 addrAC {1}[x - a]splitr addrK divr_gt0 ?subr_gt0.
 - have [//||d dP] := wlog a (x + 1); rewrite ?lte_fin ?ltr_addl //.
-  by exists d => y /dP /andP[->].
+  by exists d => y /dP /andP[->] /= /lt_le_trans; apply; rewrite lee_pinfty.
 - have [//||d dP] := wlog (x - 1) b; rewrite ?lte_fin ?gtr_addl ?ltrN10 //.
-  by exists d => y /dP /andP[_ ->].
-- by exists 1%:pos.
+  by exists d => y /dP /andP[_ ->] /=; rewrite lte_ninfty.
+- by exists 1%:pos => ? ?; rewrite lte_ninfty lte_pinfty.
 Qed.
 
 (* TODO: generalize to numFieldType? *)
@@ -2487,7 +2688,7 @@ Lemma open_ereal_lt (y : {ereal R}) : open [set u : R^o | u%:E < y]%E.
 Proof.
 case: y => [y||] /=; first exact: open_lt.
 rewrite [X in open X](_ : _ = setT); first exact: openT.
-by rewrite funeqE => ?; rewrite trueE.
+by rewrite funeqE => ?; rewrite lte_pinfty trueE.
 rewrite [X in open X](_ : _ = set0); first exact: open0.
 by rewrite funeqE => ?; rewrite falseE.
 Qed.
@@ -2498,11 +2699,11 @@ case: y => [y||] /=; first exact: open_gt.
 rewrite [X in open X](_ : _ = set0); first exact: open0.
 by rewrite funeqE => ?; rewrite falseE.
 rewrite [X in open X](_ : _ = setT); first exact: openT.
-by rewrite funeqE => ?; rewrite trueE.
+by rewrite funeqE => ?; rewrite lte_ninfty trueE.
 Qed.
 
 Lemma open_ereal_lt' (x y : {ereal R}) : (x < y)%E ->
-  ereal_locally x (fun u : R => u%:E < y)%E.
+  ereal_locally x (fun u => u < y)%E.
 Proof.
 case: x => [x|//|] xy; first exact: open_ereal_lt.
 case: y => [y||//] /= in xy *.
@@ -2510,26 +2711,143 @@ exists y; rewrite num_real; split => //= x ? //.
 by exists 0.
 case: y => [y||//] /= in xy *.
 exists y; rewrite num_real; split => //= x ? //.
-by exists 0; rewrite real0.
+exists 0; rewrite real0; split => // x.
+by move/lt_le_trans; apply; rewrite lee_pinfty.
 Qed.
 
 Lemma open_ereal_gt' (x y : {ereal R}) : (y < x)%E ->
-  ereal_locally x (fun u : R => y < u%:E)%E.
+  ereal_locally x (fun u => y < u)%E.
 Proof.
 case: x => [x||] //=; do ?[exact: open_ereal_gt];
   case: y => [y||] //=; do ?by exists 0; rewrite real0.
 by exists y; rewrite num_real.
+move=> _; exists 0; rewrite real0; split => // x.
+by apply/le_lt_trans; rewrite lee_ninfty.
 Qed.
 
 End open_sets_in_Rbar.
 
+Section open_sets_in_ereal.
+
+Variables R : realFieldType.
+Implicit Types x y : {ereal R}.
+Implicit Types r : R.
+
+Let open_ereal_lt_real r : open (fun x => x < r%:E)%E.
+Proof.
+case => [? | // | ?]; [rewrite lte_fin => xy | by exists r].
+by move: (@open_ereal_lt _ r%:E); rewrite openE; apply; rewrite lte_fin.
+Qed.
+
+Lemma open_ereal_lt_ereal x : open [set y | y < x]%E.
+Proof.
+case: x => [x | | [] // ] /=; first exact: open_ereal_lt_real.
+suff -> : ([set y | y < +oo] = \bigcup_r [set y : {ereal R} | y < r%:E])%E.
+  by apply open_bigU => x _; exact: open_ereal_lt_real.
+rewrite predeqE => -[r | | ].
+- rewrite lte_pinfty; split => // _.
+  by exists (r + 1) => //; rewrite lte_fin ltr_addl.
+- by rewrite ltxx; split => // -[] x; rewrite ltNge lee_pinfty.
+- by split => // _; exists 0 => //; rewrite lte_ninfty.
+Qed.
+
+Let open_ereal_gt_real r : open (fun x => r%:E < x)%E.
+Proof.
+case => [? | ? | //]; [rewrite lte_fin => xy | by exists r].
+by move: (@open_ereal_gt _ r%:E); rewrite openE; apply; rewrite lte_fin.
+Qed.
+
+Lemma open_ereal_gt_ereal x : open [set y | x < y]%E.
+Proof.
+case: x => [x | [] // | ] /=; first exact: open_ereal_gt_real.
+suff -> : ([set y | -oo < y] = \bigcup_r [set y : {ereal R} | r%:E < y])%E.
+  by apply open_bigU => x _; exact: open_ereal_gt_real.
+rewrite predeqE => -[r | | ].
+- rewrite lte_ninfty; split => // _.
+  by exists (r - 1) => //; rewrite lte_fin ltr_subl_addr ltr_addl.
+- by split => // _; exists 0 => //; rewrite lte_pinfty.
+- by rewrite ltxx; split => // -[] x _; rewrite ltNge lee_ninfty.
+Qed.
+
+End open_sets_in_ereal.
+
+Section ereal_is_hausdorff.
+Variable R : realFieldType.
+Implicit Types r : R.
+
+Lemma locally_image_ERFin (x : R^o) (X : set R) :
+  locally x X -> locally x%:E ((fun r => r%:E) @` X).
+Proof.
+case => _/posnumP[e] xeX; exists e%:num => //= r xer.
+by exists r => //; apply xeX.
+Qed.
+
+Lemma locally_open_ereal_lt r (f : R -> R) : r < f r ->
+  locally r%:E [set y | y < (f r)%R%:E]%E.
+Proof.
+move=> xfx; rewrite locallyE /=; eexists; split; last by move=> y; exact.
+by split; [apply open_ereal_lt_ereal | rewrite lte_fin].
+Qed.
+
+Lemma locally_open_ereal_gt r (f : R -> R) : f r < r ->
+  locally r%:E [set y | (f r)%R%:E < y]%E.
+Proof.
+move=> xfx; rewrite locallyE /=; eexists; split; last by move=> y; exact.
+by split; [apply open_ereal_gt_ereal | rewrite lte_fin].
+Qed.
+
+Lemma locally_open_ereal_pinfty r : locally +oo%E [set y | r%R%:E < y]%E.
+Proof.
+rewrite locallyE /=; eexists; split; last by move=> y; exact.
+by split; [apply open_ereal_gt_ereal | rewrite lte_pinfty].
+Qed.
+
+Lemma locally_open_ereal_ninfty r : locally -oo%E [set y | y < r%R%:E]%E.
+Proof.
+rewrite locallyE /=; eexists; split; last by move=> y; exact.
+by split; [apply open_ereal_lt_ereal | rewrite lte_ninfty].
+Qed.
+
+Lemma ereal_hausdorff : hausdorff (ereal_topologicalType R).
+Proof.
+move=> -[r| |] // [r' | |] //=.
+- move=> rr'; congr (_%:E); apply Rhausdorff => /= A B rA r'B.
+  have [/= z [[r0 ? r0z] [r1 ?]]] :=
+    rr' _ _ (locally_image_ERFin rA) (locally_image_ERFin r'B).
+  by rewrite -r0z => -[r1r0]; exists r0; split => //; rewrite -r1r0.
+- have /(@locally_open_ereal_lt _ (fun x => x + 1)) loc_r : r < r + 1.
+    by rewrite ltr_addl.
+  move/(_ _ _ loc_r (locally_open_ereal_pinfty (r + 1))) => -[z [zr rz]].
+  by move: (lt_trans rz zr); rewrite lte_fin ltxx.
+- have /(@locally_open_ereal_gt _ (fun x => x - 1)) loc_r : r - 1 < r.
+    by rewrite ltr_subl_addr ltr_addl.
+  move/(_ _ _ loc_r (locally_open_ereal_ninfty (r - 1))) => -[z [rz zr]].
+  by move: (lt_trans zr rz); rewrite ltxx.
+- have /(@locally_open_ereal_lt _ (fun x => x + 1)) loc_r' : r' < r' + 1.
+    by rewrite ltr_addl.
+  move/(_ _ _ (locally_open_ereal_pinfty (r' + 1)) loc_r') => -[z [r'z zr']].
+  by move: (lt_trans zr' r'z); rewrite ltxx.
+- move/(_ _ _ (locally_open_ereal_pinfty 0) (locally_open_ereal_ninfty 0)).
+  by move=> -[z [zx xz]]; move: (lt_trans xz zx); rewrite ltxx.
+- have /(@locally_open_ereal_gt _ (fun x => x - 1)) yB : r' - 1 < r'.
+    by rewrite ltr_subl_addr ltr_addl.
+  move/(_ _ _ (locally_open_ereal_ninfty (r' - 1)) yB) => -[z [zr' r'z]].
+  by move: (lt_trans r'z zr'); rewrite ltxx.
+- move/(_ _ _ (locally_open_ereal_ninfty 0) (locally_open_ereal_pinfty 0)).
+  by move=> -[z [zO Oz]]; move: (lt_trans Oz zO); rewrite ltxx.
+Qed.
+
+End ereal_is_hausdorff.
+
+Hint Resolve ereal_hausdorff.
+
 (** * Some limits on real functions *)
 
 Definition ereal_loc_seq (R : numDomainType) (x : {ereal R}) (n : nat) :=
   match x with
-    | x%:E => x + (n%:R + 1)^-1
-    | +oo => n%:R
-    | -oo => - n%:R
+    | x%:E => (x + (n%:R + 1)^-1)%:E
+    | +oo%E => n%:R%:E
+    | -oo%E => (- n%:R%:E)%E
   end.
 
 Lemma cvg_ereal_loc_seq (R : realType) (x : {ereal R}) :
@@ -2545,7 +2863,7 @@ case: x => /= [x [_/posnumP[d] Hp] |[d [dreal Hp]] |[d [dreal Hp]]]; last 2 firs
     by rewrite -(@natrD R N 1) ler_nat addn1.
   have /ZnatP [N Nfloor] : ifloor (maxr (- d) 0) \is a Znat.
     by rewrite Znat_def ifloor_ge0 lexU lexx orbC.
-  exists N.+1 => // n ltNn; apply: Hp; rewrite ltr_oppl.
+  exists N.+1 => // n ltNn; apply: Hp; rewrite lte_fin ltr_oppl.
   have /le_lt_trans : - d <= maxr (- d) 0 by rewrite lexU lexx.
   apply; apply: lt_le_trans (floorS_gtr _) _; rewrite floorE Nfloor.
   by rewrite -(@natrD R N 1) ler_nat addn1.
diff --git a/theories/reals.v b/theories/reals.v
index 1dad831b8..8a89337ed 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -254,7 +254,7 @@ Proof. by case: R E => ? [? ? []]. Qed.
 
 (* -------------------------------------------------------------------- *)
 Section IsInt.
-Context {R : realType}.
+Context {R : realFieldType}.
 
 Definition Rint := [qualify a x : R | `[exists z, x == z%:~R]].
 Fact Rint_key : pred_key Rint. Proof. by []. Qed.
@@ -773,9 +773,17 @@ Lemma lte_tofin (x y : R) : x < y -> (x%:E < y%:E)%E.
 Proof. by []. Qed.
 
 Lemma lee_opp2 : {mono @eopp R : x y /~ (x <= y)%E}.
-Proof. by move=> x y; elift ler_opp2 : x y. Qed.
+Proof.
+move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !ler_opp2.
+by rewrite lee_ninfty /Order.le /= realN num_real.
+by rewrite lee_pinfty /Order.le /= realN num_real.
+Qed.
 
 Lemma lte_opp2 : {mono @eopp R : x y /~ (x < y)%E}.
-Proof. by move=> x y; elift ltr_opp2 : x y. Qed.
+Proof.
+move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltr_opp2.
+by rewrite lte_ninfty /Order.lt /= realN num_real.
+by rewrite lte_pinfty /Order.lt /= realN num_real.
+Qed.
 
 End ERealOrderTheory.
diff --git a/theories/summability.v b/theories/summability.v
index 3456eb841..6362ff09b 100644
--- a/theories/summability.v
+++ b/theories/summability.v
@@ -44,7 +44,7 @@ Definition sum (I : choiceType) {K : numDomainType} {R : normedModType K}
 
 Definition summable (I : choiceType) {K : realType} {R : normedModType K}
    (x : I -> R) :=
-   \forall M \near +oo, \forall J \near totally,
+   \forall M \near +oo%R, \forall J \near totally,
    (partial_sum (fun i => `|x i|) J <= M)%R.
 
 End totally.
diff --git a/theories/topology.v b/theories/topology.v
index 108742bd9..052ff05bc 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -148,14 +148,20 @@ Require Import boolp Rstruct classical_sets posnum.
 (*                                     open sets.                             *)
 (*   topologyOfFilterMixin loc_filt loc_sing loc_loc == builds the mixin for  *)
 (*                                     a topological space from the           *)
-(*                                     properties of locally.                 *)
+(*                                     properties of locally and hence        *)
+(*                                     assumes that the carrier is a          *)
+(*                                     filterType.                            *)
 (*   topologyOfOpenMixin opT opI op_bigU == builds the mixin for a            *)
 (*                                     topological space from the properties  *)
-(*                                     of open sets.                          *)
+(*                                     of open sets, assuming the carrier is  *)
+(*                                     a pointed type. locally_of_open must   *)
+(*                                     be used to declare a filterType.       *)
 (*   topologyOfBaseMixin b_cover b_join == builds the mixin for a topological *)
 (*                                     space from the properties of a base of *)
 (*                                     open sets; the type of indices must be *)
-(*                                     a pointedType.                         *)
+(*                                     a pointedType, as well as the carrier. *)
+(*                                     locally_of_open \o open_from must be   *)
+(*                                     used to declare a filterType           *)
 (*       topologyOfSubbaseMixin D b == builds the mixin for a topological     *)
 (*                                     space from a subbase of open sets b    *)
 (*                                     indexed on domain D; the type of       *)
@@ -394,6 +400,8 @@ Notation "[ 'filteredType' U 'of' T 'for' cT ]" :=  (@clone U T cT _ idfun)
 Notation "[ 'filteredType' U 'of' T ]" := (@clone U T _ _ id)
   (at level 0, format "[ 'filteredType'  U  'of'  T ]") : form_scope.
 
+
+
 (* The default filter for an arbitrary element is the one obtained *)
 (* from its type *)
 Canonical default_arrow_filter Y (Z : pointedType) (X : source Z Y) :=
@@ -1011,6 +1019,14 @@ move=> eq_fg P /=; apply: filterS2 eq_fg => x eq_fg [y [fxy Py]].
 by exists y; rewrite -eq_fg.
 Qed.
 
+Lemma cvg_near_const (T U : Type) (f : T -> U) (F : set (set T)) (G : set (set U)) :
+  Filter F -> ProperFilter G ->
+  (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G.
+Proof.
+move=> FF FG fFG P /= GP; rewrite !near_simpl; apply: (have_near G).
+by apply: filter_app fFG; near=> y => /=; apply: filterS => x /= ->; near: y.
+Grab Existential Variables. all: by end_near. Qed.
+
 (** ** Specific filters *)
 
 Section at_point.
@@ -1402,8 +1418,8 @@ Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°.
 Proof.
 rewrite /interior predeqE => //= x; rewrite locallyE; split => [[B0 [?]] | []].
 - by rewrite subsetI => // -[? ?]; split; rewrite locallyE; exists B0.
-- rewrite locallyE => -[B0 [? ?]] [B1 [? ?]]; exists (B0 `&` B1); split;
-  [exact: neighI | by rewrite subsetI; split; apply: subIset; [left|right]].
+- rewrite locallyE => -[B0 [? ?]] [B1 [? ?]]; exists (B0 `&` B1); split;
+  [exact: neighI | by rewrite subsetI; split; apply: subIset; [left|right]].
 Qed.
 
 End Topological1.
@@ -1486,6 +1502,21 @@ Qed.
 Arguments cst_continuous {T T'} k F {FF}.
 Hint Resolve cst_continuous : core.
 
+Lemma cvg_fconst (T : Type) (U : topologicalType)
+  (f : T -> U) (F : set (set T)) (l : U) :
+  Filter F ->
+  (\forall x \near F, f x = l) -> f @ F --> l.
+Proof.
+move=> FF fFl P /=; rewrite !near_simpl => Pl.
+by apply: filterS fFl => _ ->; apply: locally_singleton.
+Qed.
+
+Lemma cvg_const (T : Type) (U : topologicalType) (F : set (set T)) {FF : Filter F}
+  (x : U) : (fun _ : T => x) @ F --> x.
+Proof. by apply: cvg_fconst; near=> x0.
+Grab Existential Variables. all: end_near. Qed.
+Arguments cvg_const {T U F FF} x.
+
 (** ** Topology defined by a filter *)
 
 Section TopologyOfFilter.
@@ -2344,6 +2375,121 @@ Qed.
 
 End Covers.
 
+Section separated_topologicalType.
+Variable (T : topologicalType).
+
+Local Open Scope classical_set_scope.
+
+Definition close_to (x : T) (A : set T) : Prop :=
+  forall N, neigh x N -> N `&` A !=set0.
+
+Definition close (x y : T) : Prop :=
+  forall M, neigh y M -> close_to x M.
+
+Lemma close_refl (t : T) : close t t.
+Proof. by move=> M [? ?] N [? ?]; exists t; split. Qed.
+Hint Resolve close_refl : core.
+
+Lemma close_sym (x y : T) : close x y -> close y x.
+Proof.
+rewrite /close /close_to => xy N xN M yM.
+rewrite setIC; apply xy => //; by case yM.
+Qed.
+
+Lemma cvg_close {F} {FF : ProperFilter F} (x y : T) :
+  F --> x -> F --> y -> close x y.
+Proof.
+move=> Fx Fy N yN M xM; near F => z; exists z; split.
+- near: z; by apply/Fx; rewrite /filter_of locallyE; exists M; split.
+- near: z; by apply/Fy; rewrite /filter_of locallyE; exists N; split.
+Grab Existential Variables. all: end_near. Qed.
+
+Lemma close_cvg (F1 F2 : set (set T)) {FF2 : ProperFilter F2} :
+  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
+Proof.
+move=> F12 F21.
+have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
+  by apply: (@cvg_close F2) => //; apply: cvgP F2l.
+have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
+rewrite dvgP // dvgP //; exact/close_refl.
+Qed.
+
+Lemma cvgx_close (x y : T) : x --> y -> close x y.
+Proof. exact: cvg_close. Qed.
+
+Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
+  {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
+Proof.
+move=> f_prop fFl fFl'.
+suff f_totalfun: infer {near F, is_totalfun f} by exact: cvg_close fFl fFl'.
+apply: filter_app f_prop; near=> x; split=> //=; near: x.
+have: (f `@ F) setT by apply: fFl; apply: filterT.
+by rewrite fmapiE; apply: filterS => x [y []]; exists y.
+Grab Existential Variables. all: end_near. Qed.
+Definition cvg_toi_locally_close := @cvgi_close.
+
+Lemma open_hausdorff : hausdorff T =
+  (forall x y : T, x != y ->
+    exists2 AB, (x \in AB.1 /\ y \in AB.2) &
+                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0]).
+Proof.
+rewrite propeqE; split => [T_filterT2|T_openT2] x y.
+  have := contrap (T_filterT2 x y); rewrite (rwP eqP) (rwP negP) => cl /cl.
+  rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
+  rewrite forallbE => /existsp_asboolPn/=[A]/negP/existsp_asboolPn/=[B].
+  rewrite [locally _ _ -> _](rwP imply_asboolP) => /negP.
+  rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].
+  move=> /asboolPn; rewrite -set0P => /negP; rewrite negbK => /eqP AIB_eq0.
+  move: xA yB; rewrite !locallyE.
+  move=> - [oA [[oA_open oAx] oAA]] [oB [[oB_open oBx] oBB]].
+  by exists (oA, oB); rewrite ?in_setE; split => //; apply: subsetI_eq0 AIB_eq0.
+apply: contrapTT => /eqP /T_openT2[[/=A B]].
+rewrite !in_setE => - [xA yB] [Aopen Bopen /eqP AIB_eq0].
+move=> /(_ A B (neigh_locally _) (neigh_locally _)).
+by rewrite -set0P => /(_ _ _)/negP; apply.
+Qed.
+
+Hypothesis sep : hausdorff T.
+
+Lemma closeE (x y : T) : close x y = (x = y).
+Proof.
+rewrite propeqE; split => [cxy|->//]; have [//|xdy] := eqVneq x y.
+apply: sep => A B; rewrite !locallyE => - [oA [xoA oAA]] [oB [xoB oBB]].
+exact: subsetI_neq0 oAA oBB (cxy _ _ _ _).
+Qed.
+
+Lemma close_eq (y x : T) : close x y -> x = y.
+Proof. by rewrite closeE. Qed.
+
+Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
+Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
+
+Lemma cvg_eq (x y : T) : x --> y -> x = y.
+Proof. by rewrite -closeE //; apply: cvg_close. Qed.
+
+Lemma lim_id (x : T) : lim x = x.
+Proof. by apply/esym/cvg_eq/cvg_ex; exists x. Qed.
+
+Lemma cvg_lim {F} {FF : ProperFilter F} (l : T) : F --> l -> lim F = l.
+Proof. by move=> Fl; have Fcv := cvgP Fl; apply: (@cvg_unique F). Qed.
+
+Lemma cvg_map_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
+  f @ F --> l -> lim (f @ F) = l.
+Proof. exact: cvg_lim. Qed.
+
+Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
+  {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
+Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
+
+Lemma cvgi_map_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
+  F (fun x : U => is_subset1 (f x)) ->
+  f `@ F --> l -> lim (f `@ F) = l.
+Proof.
+move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
+Qed.
+
+End separated_topologicalType.
+
 (* connected sets *)
 
 Definition connected (T : topologicalType) (A : set T) :=
@@ -2506,7 +2652,13 @@ Proof. exact: PseudoMetric.ax3. Qed.
 Lemma locally_ball (x : M) (eps : {posnum R}) : locally x (ball x eps%:num).
 Proof. by apply/locallyP; exists eps%:num. Qed.
 
-Definition close (x y : M) : Prop := forall eps : {posnum R}, ball x eps%:num y.
+Lemma neigh_ball (x : M) (eps : {posnum R}) : neigh x ((ball x eps%:num)^°).
+Proof.
+split; first exact: open_interior.
+apply: locally_singleton; apply: locally_interior.
+by apply/locallyP; exists eps%:num.
+Qed.
+
 
 Lemma ball_ler (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2.
 Proof.
@@ -2517,11 +2669,6 @@ Qed.
 Lemma ball_le (x : M) (e1 e2 : R) : (e1 <= e2) -> ball x e1 `<=` ball x e2.
 Proof. by move=> /ball_ler. Qed.
 
-Lemma close_refl (x : M) : close x x. Proof. by []. Qed.
-
-Lemma close_sym (x y : M) : close x y -> close y x.
-Proof. by move=> ??; apply: ball_sym. Qed.
-
 Definition entourages : set (set (M * M)):=
   filter_from [set eps : R | eps > 0]
               (fun eps => [set xy | ball xy.1 eps xy.2]).
@@ -2576,13 +2723,6 @@ Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y :
   forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z].
 Proof. by move/cvgi_ballP. Qed.
 
-Lemma cvg_const {T} {F : set (set T)}
-   {FF : Filter F} (a : M) : a @[_ --> F] --> a.
-Proof.
-move=> P /locallyP[_ /posnumP[eps] subP]; rewrite !near_simpl /=.
-by apply: filterE=> ?; apply/subP/close_refl.
-Qed.
-
 Definition ball_set (A : set M) e := \bigcup_(p in A) ball p e.
 Canonical set_filter_source :=
   @Filtered.Source Prop _ M (fun A => locally_ ball_set A).
@@ -2590,7 +2730,7 @@ Canonical set_filter_source :=
 End pseudoMetricType_numDomainType.
 Hint Resolve locally_ball : core.
 Hint Resolve close_refl : core.
-Arguments cvg_const {R M T F FF} a.
+Arguments close_cvg {T} F1 F2 {FF2} _.
 
 Section pseudoMetricType_numFieldType.
 Context {R : numFieldType} {M : pseudoMetricType R}.
@@ -2607,55 +2747,73 @@ Lemma ball_splitl (z x y : M) (e : R) :
   ball x (e / 2) z -> ball y (e / 2) z -> ball x e y.
 Proof. by move=> bxz /ball_sym /(ball_split bxz). Qed.
 
-Lemma cvg_close {F} {FF : ProperFilter F} (x y : M) :
-  F --> x -> F --> y -> close x y.
+Lemma ball_close (x y : M) :
+  close x y = forall eps : {posnum R}, ball x eps%:num y.
 Proof.
-move=> Fx Fy e; near F => z; apply: (@ball_splitl z); near: z;
-by [apply/Fx/locally_ball|apply/Fy/locally_ball].
-Grab Existential Variables. all: end_near. Qed.
+rewrite propeqE; split => [cxy eps|cxy].
+  have [z [zx zy]] := cxy _ (neigh_ball _ (eps%:num/2)%:pos)
+                          _ (neigh_ball _ (eps%:num/2)%:pos).
+  by apply: (@ball_splitl z); apply: interior_subset.
+move=> B /neigh_locally/locallyP[_/posnumP[e2 e2B]].
+move=> A /neigh_locally/locallyP[_/posnumP[e1 e1A]].
+by exists y; split; [apply/e1A|apply/e2B/ballxx].
+Qed.
 
-Lemma close_trans (x y z : M) : close x y -> close y z -> close x z.
-Proof. by move=> cxy cyz eps; apply: ball_split (cxy _) (cyz _). Qed.
+Lemma close_trans (y x z : M) : close x y -> close y z -> close x z.
+Proof.
+by rewrite !ball_close  => cxy cyz eps; apply: ball_split (cxy _) (cyz _).
+Qed.
 
 Lemma close_cvgxx (x y : M) : close x y -> x --> y.
 Proof.
-move=> cxy P /= /locallyP /= [_/posnumP [eps] epsP].
+rewrite ball_close => cxy P /= /locallyP /= [_/posnumP [eps] epsP].
 apply/locallyP; exists (eps%:num / 2) => // z bxz.
 by apply: epsP; apply: ball_splitr (cxy _) bxz.
 Qed.
 
-Lemma cvgx_close (x y : M) : x --> y -> close x y.
-Proof. exact: cvg_close. Qed.
-
-Lemma cvgi_close T {F} {FF: ProperFilter F} (f : T -> set M) (l l' : M) :
-  {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
-Proof.
-move=> f_prop fFl fFl'.
-suff f_totalfun: infer {near F, is_totalfun f} by exact: cvg_close fFl fFl'.
-apply: filter_app f_prop; near=> x; split=> //=.
-by have [//|y [fxy _]] := near (cvgi_ball fFl [gt0 of 1]) x; exists y.
-Grab Existential Variables. all: end_near. Qed.
-Definition cvg_toi_locally_close := @cvgi_close.
-
-Lemma close_cvg (F1 F2 : set (set M)) {FF2 : ProperFilter F2} :
-  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
-Proof.
-move=> F12 F21; have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
-  by apply: (@cvg_close F2) => //; apply: cvgP F2l.
-have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
-rewrite dvgP // dvgP //; exact/close_refl.
-Qed.
-
 Lemma cvg_closeP (F : set (set M)) (l : M) : ProperFilter F ->
   F --> l <-> ([cvg F in M] /\ close (lim F) l).
 Proof.
 move=> FF; split=> [Fl|[cvF]Cl].
-  by have /cvgP := Fl; split=> //; apply: (@cvg_close F).
+  by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F).
 by apply: cvg_trans (close_cvgxx Cl).
 Qed.
 
 End pseudoMetricType_numFieldType.
-Arguments close_cvg {R M} F1 F2 {FF2} _.
+
+Section ball_hausdorff.
+Variables (R : numDomainType) (T : pseudoMetricType R).
+
+Lemma ball_hausdorff : hausdorff T =
+  forall (a b : T), a != b ->
+  exists r : {posnum R} * {posnum R}, ball a r.1%:num `&` ball b r.2%:num == set0.
+Proof.
+rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
+  move=> A B; rewrite 2!in_setE => [[aA bB] [oA oB /eqP ABeq0]].
+  have /locallyP[_/posnumP[r] rA]: locally a A by apply: neigh_locally.
+  have /locallyP[_/posnumP[s] rB]: locally b B by apply: neigh_locally.
+  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 in_setE; apply: locally_singleton; apply: locally_interior;
+            apply/locallyP; apply: in_filter_from.
+split; do ?by apply: open_interior.
+by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset.
+Qed.
+End ball_hausdorff.
+
+Lemma close_cluster (R : numFieldType) (T : pseudoMetricType R) (x y : T) :
+  close x y = cluster (locally x) y.
+Proof.
+rewrite propeqE; split => xy.
+- move=> A B xA; rewrite -locally_ballE locally_E => -[_/posnumP[e] yeB].
+  exists x; split; first exact: locally_singleton.
+  by apply/yeB/ball_sym; move: e {yeB}; rewrite -ball_close.
+- rewrite ball_close => e.
+  have e20 : 0 < e%:num / 2 by apply: divr_gt0.
+  set e2  := PosNum e20.
+  case: (xy _ _ (locally_ball x e2) (locally_ball y e2)) => z [xz /ball_sym zy].
+  by rewrite (splitr e%:num); exact: (ball_triangle xz).
+Qed.
 
 Section entourages.
 Variable R : numDomainType.