diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c0a8067961..87768d5cf1 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -38,6 +38,27 @@
 - in `constructive_ereal.v`:
   + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`,
     `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr`
+- in `topology.v`:
+  + lemmas `continuous_subspace0`, `continuous_subspace1`
+
+- in `realfun.v`:
+  + Instance for `GRing.opp` over real intervals
+
+### Changed
+- in `realfun.v`
+  + lemmas `itv_continuous_inj_le`, `itv_continuous_inj_ge`,
+     `itv_continuous_inj_mono`, `segment_continuous_inj_le`,
+     `segment_continuous_inj_ge`, `segment_can_le` ,
+     `segment_can_ge`, `segment_can_mono`,
+     `segment_continuous_surjective`, `segment_continuous_le_surjective`,
+     `segment_continuous_ge_surjective`, `continuous_inj_image_segment`,
+     `continuous_inj_image_segmentP`, `segment_continuous_can_sym`,
+     `segment_continuous_le_can_sym`, `segment_continuous_ge_can_sym`,
+     `segment_inc_surj_continuous`, `segment_dec_surj_continuous`,
+     `segment_mono_surj_continuous`, `segment_can_le_continuous`,
+     `segment_can_ge_continuous`, `segment_can_continuous`
+     all have "{in I, continuous f}" replaced by "{within I, continuous f}"
+
 
 ### Renamed
 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 82e2c57808..321f66a304 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2506,7 +2506,7 @@ Section at_left_right.
 Variable R : numFieldType.
 
 Definition at_left (x : R) := within (fun u => u < x) (nbhs x).
-Definition at_right (x : R) := within (fun u : R => x < u) (nbhs x).
+Definition at_right (x : R) := within (fun u => x < u) (nbhs x).
 
 (* :TODO: We should have filter notation ^- and ^+ for these *)
 
diff --git a/theories/realfun.v b/theories/realfun.v
index f32caccf13..59b43459d6 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -3,7 +3,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 Require Import boolp ereal reals mathcomp_extra functions.
 Require Import classical_sets signed topology prodnormedzmodule.
-Require Import cardinality normedtype derive.
+Require Import cardinality normedtype derive set_interval.
+From HB Require Import structures.
 
 (******************************************************************************)
 (* This file provides properties of standard real-valued functions over real  *)
@@ -26,9 +27,10 @@ Section real_inverse_functions.
 Variable R : realType.
 Implicit Types (a b : R) (f g : R -> R).
 
-(* TODO: this is a workaround to weaken {in I, continuous f} to use IVT.
-   Updating this whole file to use {within [set` I], continuous f} is the
-   better, but more labor intensive approach *)
+(* This lemma should be used with caution. Generally `{within I, continuous f}`
+   is what one would intend. So having `{in I, continuous f}` as a condition
+   may indicate potential issues at the endpoints of the interval.
+*)
 Lemma continuous_subspace_itv (I : interval R) (f : R -> R) :
   {in I, continuous f} -> {within [set` I], continuous f}.
 Proof.
@@ -38,28 +40,29 @@ Qed.
 
 Lemma itv_continuous_inj_le f (I : interval R) :
   (exists x y, [/\ x \in I, y \in I, x < y & f x <= f y]) ->
-  {in I, continuous f} -> {in I &, injective f} ->
+  {within [set` I], continuous f} -> {in I &, injective f} ->
   {in I &, {mono f : x y / x <= y}}.
 Proof.
 gen have fxy : f / {in I &, injective f} ->
     {in I &, forall x y, x < y -> f x != f y}.
   move=> fI x y xI yI xLy; apply/negP => /eqP /fI => /(_ xI yI) xy.
   by move: xLy; rewrite xy ltxx.
-gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} ->
+gen have main : f / forall c, {within [set` I], continuous f} ->
+    {in I &, injective f} ->
     {in I &, forall a b, f a < f b -> a < c -> c < b -> f a < f c /\ f c < f b}.
   move=> c fC fI a b aI bI faLfb aLc cLb.
   have intP := interval_is_interval aI bI.
   have cI : c \in I by rewrite intP// (ltW aLc) ltW.
   have ctsACf : {within `[a, c], continuous f}.
-    apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
+    apply: (continuous_subspaceW _ fC) => x; rewrite /= inE => /itvP axc.
     by rewrite intP// axc/= (le_trans _ (ltW cLb))// axc.
-  have ctsCBf : {within `[c,b], continuous f}.
-    apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
+  have ctsCBf : {within `[c, b], continuous f}.
+    apply: (continuous_subspaceW _ fC) => x /=; rewrite inE => /itvP axc.
     by rewrite intP// axc andbT (le_trans (ltW aLc)) ?axc.
   have [aLb alb'] : a < b /\ a <= b by rewrite ltW (lt_trans aLc).
   have [faLfc|fcLfa|/eqP faEfc] /= := ltrgtP (f a) (f c).
   - split; rewrite // lt_neqAle fxy // leNgt; apply/negP => fbLfc.
-    move: (fbLfc); suff /eqP -> : c == b by rewrite ltxx.
+    have := fbLfc; suff /eqP -> : c == b by rewrite ltxx.
     rewrite eq_le (ltW cLb) /=.
     have [d /andP[ad dc] fdEfb] : exists2 d, a <= d <= c & f d = f b.
       have aLc' : a <= c by rewrite ltW.
@@ -88,7 +91,8 @@ have aux a c b : a \in I -> b \in I -> a < c -> c < b ->
   have cI : c \in I by rewrite (interval_is_interval aI bI)// (ltW aLc)/= ltW.
   have fanfb : f a != f b by apply: (fxy f fI).
   have decr : f b  < f a -> f b < f c /\ f c < f a.
-    have ofC : {in I, continuous (-f)} by move=>> ?; apply/continuousN/fC.
+    have ofC : {within [set` I], continuous (-f)}.
+      move=> ?; apply: continuous_comp; [exact: fC | exact: continuousN].
     have ofI : {in I &, injective (-f)} by move=>> ? ? /oppr_inj/fI ->.
     rewrite -[X in X < _ -> _](opprK (f b)) ltr_oppl => ofaLofb.
     have := main _ c ofC ofI a b aI bI ofaLofb aLc cLb.
@@ -120,7 +124,7 @@ Qed.
 
 Lemma itv_continuous_inj_ge f (I : interval R) :
   (exists x y, [/\ x \in I, y \in I, x < y & f y <= f x]) ->
-  {in I, continuous f} -> {in I &, injective f} ->
+  {within [set` I], continuous f} -> {in I &, injective f} ->
   {in I &, {mono f : x y /~ x <= y}}.
 Proof.
 move=> [a [b [aI bI ab fbfa]]] fC fI x y xI yI.
@@ -132,7 +136,7 @@ by move/oppr_inj; apply/fI.
 Qed.
 
 Lemma itv_continuous_inj_mono f (I : interval R) :
-    {in I, continuous f} -> {in I &, injective f} -> monotonous I f.
+    {within [set` I], continuous f} -> {in I &, injective f} -> monotonous I f.
 Proof.
 move=> fC fI.
 case: (pselect (exists a b, [/\ a \in I , b \in I & a < b])); last first.
@@ -145,7 +149,7 @@ by right; apply: itv_continuous_inj_ge => //; exists a, b; rewrite ?fbLfa.
 Qed.
 
 Lemma segment_continuous_inj_le f a b :
-    f a <= f b -> {in `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
+    f a <= f b -> {within `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
   {in `[a, b] &, {mono f : x y / x <= y}}.
 Proof.
 move=> fafb fct finj; have [//|] := itv_continuous_inj_mono fct finj.
@@ -157,7 +161,7 @@ by move=> /(_ (ltW aLb) (ltW aLb)); rewrite lt_geF.
 Qed.
 
 Lemma segment_continuous_inj_ge f a b :
-    f a >= f b -> {in `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
+    f a >= f b -> {within `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
   {in `[a, b] &, {mono f : x y /~ x <= y}}.
 Proof.
 move=> fafb fct finj; have [|//] := itv_continuous_inj_mono fct finj.
@@ -171,7 +175,7 @@ Qed.
 (* The condition "f a <= f b" is unnecessary because the last                *)
 (* interval condition is vacuously true otherwise.                           *)
 Lemma segment_can_le a b f g : a <= b ->
-    {in `[a, b], continuous f} ->
+    {within `[a, b], continuous f} ->
     {in `[a, b], cancel f g} ->
   {in `[f a, f b] &, {mono g : x y / x <= y}}.
 Proof.
@@ -183,27 +187,35 @@ have lt_ab : a < b by case: (ltgtP a b) aLb faLfb => // ->; rewrite ltxx.
 have w : exists x y, [/\ x \in `[a, b], y \in `[a, b], x < y & f x <= f y].
   by exists a, b; rewrite !bound_itvE (ltW faLfb).
 have fle := itv_continuous_inj_le w ctf (can_in_inj fK).
-move=> x y xin yin; have := IVT aLb (continuous_subspace_itv ctf).
+move=> x y xin yin; have := IVT aLb ctf.
 case: (ltrgtP (f a) (f b)) faLfb => // _ _ ivt.
 by have [[u uin <-] [v vin <-]] := (ivt _ xin, ivt _ yin); rewrite !fK// !fle.
 Qed.
 
+Section negation_itv.
+Local Lemma opp_fun (a b : R) : set_fun `[-b, -a] `[a, b]  (@GRing.opp R).
+Proof. by move=> x /=; rewrite oppr_itvcc. Qed.
+
+HB.instance Definition _ a b := IsFun.Build _ _ _ _ _ (@opp_fun a b).
+End negation_itv.
+
 (* The condition "f b <= f a" is unnecessary---see seg...increasing above    *)
 Lemma segment_can_ge a b f g : a <= b ->
-    {in `[a, b], continuous f} ->
+    {within `[a, b], continuous f} ->
     {in `[a, b], cancel f g} ->
   {in `[f b, f a] &, {mono g : x y /~ x <= y}}.
 Proof.
 move=> aLb fC fK x y xfbfa yfbfa; rewrite -ler_opp2.
 apply: (@segment_can_le (- b) (- a) (f \o -%R) (- g));
-    rewrite /= ?ler_opp2 ?opprK//.
-  move=> z zab; apply: continuous_comp; first exact: continuousN.
-  by apply: fC; rewrite oppr_itvcc.
+    rewrite /= ?ler_opp2 ?opprK //.
+  pose fun_neg : (subspace `[-b,-a] -> subspace `[a,b]) := @GRing.opp R.
+  move=> z; apply: (@continuous_comp _ _ _ [fun of fun_neg]); last exact: fC.
+  exact/subspaceT_continuous/continuous_subspaceT/opp_continuous.
 by move=> z zab; rewrite -[- g]/(@GRing.opp _ \o g)/= fK ?opprK// oppr_itvcc.
 Qed.
 
 Lemma segment_can_mono a b f g : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
+    {within `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
   monotonous (f @`[a, b]) g.
 Proof.
 move=> le_ab fct fK; rewrite /monotonous/=; case: ltrgtP => fab; [left|right..];
@@ -212,25 +224,25 @@ by move=> x y /itvxxP<- /itvxxP<-; rewrite !lexx.
 Qed.
 
 Lemma segment_continuous_surjective a b f : a <= b ->
-  {in `[a, b], continuous f} -> set_surj `[a, b] (f @`[a, b]) f.
-Proof. by move=> ? /continuous_subspace_itv fct y/= /IVT[]// x; exists x. Qed.
+  {within `[a, b], continuous f} -> set_surj `[a, b] (f @`[a, b]) f.
+Proof. by move=> ? fct y/= /IVT[]// x; exists x. Qed.
 
 Lemma segment_continuous_le_surjective a b f : a <= b -> f a <= f b ->
-  {in `[a, b], continuous f} -> set_surj `[a, b] `[f a, f b] f.
+  {within `[a, b], continuous f} -> set_surj `[a, b] `[f a, f b] f.
 Proof.
 move=> le_ab f_ab /(segment_continuous_surjective le_ab).
 by rewrite (min_idPl _)// (max_idPr _).
 Qed.
 
 Lemma segment_continuous_ge_surjective a b f : a <= b -> f b <= f a ->
-  {in `[a, b], continuous f} -> set_surj `[a, b] `[f b, f a] f.
+  {within `[a, b], continuous f} -> set_surj `[a, b] `[f b, f a] f.
 Proof.
 move=> le_ab f_ab /(segment_continuous_surjective le_ab).
 by rewrite (min_idPr _)// (max_idPl _).
 Qed.
 
 Lemma continuous_inj_image_segment a b f : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
+    {within `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
   f @` `[a, b] = f @`[a, b]%classic.
 Proof.
 move=> leab fct finj; apply: mono_surj_image_segment => //.
@@ -239,7 +251,7 @@ exact: segment_continuous_surjective.
 Qed.
 
 Lemma continuous_inj_image_segmentP a b f : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
+    {within `[a, b], continuous f} -> {in `[a, b] &, injective f} ->
   forall y, reflect (exists2 x, x \in `[a, b] & f x = y) (y \in f @`[a, b]).
 Proof.
 move=> /continuous_inj_image_segment/[apply]/[apply]/predeqP + y => /(_ y) faby.
@@ -247,7 +259,7 @@ by apply/(equivP idP); symmetry.
 Qed.
 
 Lemma segment_continuous_can_sym a b f g : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
+    {within `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
   {in f @`[a, b], cancel g f}.
 Proof.
 move=> aLb ctf fK; have g_mono := segment_can_mono aLb ctf fK.
@@ -262,7 +274,7 @@ by apply/ssrbool.inj_can_sym_in_on => x xab; rewrite ?fK ?mono_mem_image_segment
 Qed.
 
 Lemma segment_continuous_le_can_sym a b f g : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
+    {within `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
   {in `[f a, f b], cancel g f}.
 Proof.
 move=> aLb fct fK x xfafb; apply: (segment_continuous_can_sym aLb fct fK).
@@ -271,7 +283,7 @@ by case: ltrgtP xfafb => // ->.
 Qed.
 
 Lemma segment_continuous_ge_can_sym a b f g : a <= b ->
-    {in `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
+    {within `[a, b], continuous f} -> {in `[a, b], cancel f g} ->
   {in `[f b, f a], cancel g f}.
 Proof.
 move=> aLb fct fK x xfafb; apply: (segment_continuous_can_sym aLb fct fK).
@@ -280,17 +292,18 @@ by case: ltrgtP xfafb => // ->.
 Qed.
 
 Lemma segment_inc_surj_continuous a b f :
-    {in `[a, b] &, {mono f : x y / x <= y}} ->
-    set_surj `[a, b] `[f a, f b] f ->
-  {in `]a, b[, continuous f}.
+    {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f ->
+  {within `[a, b], continuous f}.
 Proof.
 move=> fle f_surj; have [f_inj flt] := (inc_inj_in fle, leW_mono_in fle).
-have [aLb|bLa] := ltP a b; last by move=> z; rewrite itv_ge//= -leNgt.
+have [aLb|bLa|] := ltgtP a b; first last.
+- by move=> ->; rewrite set_itv1; exact: continuous_subspace1.
+- rewrite continuous_subspace_in => z /set_mem /=; rewrite in_itv /=.
+  by move=> /andP[/le_trans] /[apply]; rewrite leNgt bLa.
 have le_ab : a <= b by rewrite ltW.
 have [aab bab] : a \in `[a, b] /\ b \in `[a, b] by rewrite !bound_itvE ltW.
 have fab : f @` `[a, b] = `[f a, f b]%classic by exact:inc_surj_image_segment.
-pose g := pinv `[a, b] f.
-have fK : {in `[a, b], cancel f g}.
+pose g := pinv `[a, b] f; have fK : {in `[a, b], cancel f g}.
   by rewrite -[mem _]mem_setE; apply: pinvKV; rewrite !mem_setE.
 have gK : {in `[f a, f b], cancel g f} by move=> z zab; rewrite pinvK// fab inE.
 have gle : {in `[f a, f b] &, {mono g : x y / x <= y}}.
@@ -298,9 +311,10 @@ have gle : {in `[f a, f b] &, {mono g : x y / x <= y}}.
   move=> z zfab; have {zfab} : `[f a, f b]%classic z by [].
   by rewrite -fab => -[x xab <-]; rewrite fK.
 have glt := leW_mono_in gle.
-move=> x xab; have xabcc : x \in `[a, b] by apply: subset_itv_oo_cc.
-have fxab : f x \in `](f a), (f b)[ by rewrite in_itv/= !flt.
-have fxabcc : f x \in `[f a, f b] by apply: subset_itv_oo_cc.
+rewrite continuous_subspace_in => x xab.
+have xabcc : x \in `[a, b] by move: xab; rewrite mem_setE.
+have fxab : f x \in `[f a, f b] by rewrite in_itv/= !fle.
+have := xabcc; rewrite in_itv //= => /andP [ax xb].
 apply/cvg_distP => _ /posnumP[e]; rewrite !near_simpl; near=> y.
 rewrite (@le_lt_trans _ _ (e%:num / 2%:R))//; last first.
   by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n.
@@ -308,25 +322,55 @@ rewrite ler_distlC; near: y.
 pose u := minr (f x + e%:num / 2) (f b).
 pose l := maxr (f x - e%:num / 2) (f a).
 have ufab : u \in `[f a, f b].
-  rewrite !in_itv/= le_minl ?le_minr lexx ?fle// le_ab orbT ?andbT.
-  by rewrite ler_paddr// fle ?in_itv/= ?(itvP xab)// lexx.
+  rewrite !in_itv /= le_minl ?le_minr lexx ?fle // le_ab orbT ?andbT.
+  by rewrite ler_paddr // fle.
 have lfab : l \in `[f a, f b].
-  rewrite !in_itv/= le_maxl ?le_maxr lexx ?fle// le_ab orbT ?andbT/=.
-  by rewrite ler_subl_addr ler_paddr// fle ?(itvP xab)// lexx.
-near=> y; suff: l <= f y <= u by rewrite le_maxl le_minr -!andbA => /and4P[-> _ ->].
-have yab : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv.
+  rewrite !in_itv/= le_maxl ?le_maxr lexx ?fle// le_ab orbT ?andbT.
+  by rewrite ler_subl_addr ler_paddr// fle // lexx.
+have guab : g u \in `[a, b].
+  rewrite !in_itv; apply/andP; split; have := ufab; rewrite in_itv => /andP.
+    by case; rewrite /= -gle // ?fK // bound_itvE fle.
+  by case => _; rewrite /= -gle // ?fK // bound_itvE fle.
+have glab : g l \in `[a, b].
+  rewrite !in_itv; apply/andP; split; have := lfab; rewrite in_itv /= => /andP.
+    by case; rewrite -gle // ?fK // bound_itvE fle.
+  by case => _; rewrite -gle // ?fK // bound_itvE fle.
+have faltu : f a < u.
+  rewrite /u comparable_lt_minr ?real_comparable ?num_real// flt// aLb andbT.
+  by rewrite (@le_lt_trans _ _ (f x)) ?fle// ltr_addl.
+have lltfb : l < f b.
+  rewrite /u comparable_lt_maxl ?real_comparable ?num_real// flt// aLb andbT.
+  by rewrite (@lt_le_trans _ _ (f x)) ?fle// ltr_subl_addr ltr_addl.
+case: pselect => // _; rewrite near_withinE; near_simpl.
+have := ax; rewrite le_eqVlt => /orP[/eqP|] {}ax.
+  near=> y => /[dup] yab; rewrite /= in_itv => /andP[ay yb]; apply/andP; split.
+    by rewrite (@le_trans _ _ (f a)) ?fle// ler_subl_addr ax ler_paddr.
+  apply: ltW; suff : f y < u by rewrite lt_minr => /andP[->].
+  rewrite -?[f y < _]glt// ?fK//; last by rewrite in_itv /= !fle.
+  by near: y; near_simpl; apply: open_lt; rewrite /= -flt ?gK// -ax.
+have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb].
+  near=> y => /[dup] yab; rewrite /= in_itv /= => /andP[ay yb].
+  apply/andP; split; last by rewrite (@le_trans _ _ (f b)) ?fle// xb ler_paddr.
+  apply: ltW; suff : l < f y by rewrite lt_maxl => /andP[->].
+  rewrite -?[_ < f y]glt// ?fK//; last by rewrite in_itv /= !fle.
+  by near: y; near_simpl; apply: open_gt; rewrite /= -flt// gK// xb.
+have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split.
+near=> y; suff: l <= f y <= u.
+  by rewrite le_maxl le_minr -!andbA => /and4P[-> _ ->].
+have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv.
 have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW.
-rewrite -[l <= _]gle -?[_ <= u]gle// ?fK//.
-apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv/= -[x]fK//.
-by rewrite !glt//= lt_minr lt_maxl !(itvP fxab) ?andbT ltr_subl_addr ltr_spaddr.
+rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //.
+apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=.
+rewrite -[x]fK // !glt//= lt_minr lt_maxl ?andbT ltr_subl_addr ltr_spaddr //.
+by apply/and3P; split; rewrite // flt.
 Unshelve. all: by end_near. Qed.
 
 Lemma segment_dec_surj_continuous a b f :
     {in `[a, b] &, {mono f : x y /~ x <= y}} ->
     set_surj `[a, b] `[f b, f a] f ->
-  {in `]a, b[, continuous f}.
+  {within `[a, b], continuous f}.
 Proof.
-move=> fge f_surj; suff: {in `]a, b[, continuous (- f)}.
+move=> fge f_surj; suff: {within `[a, b], continuous (- f)}.
   move=> contNf x xab; rewrite -[f]opprK.
   exact/continuous_comp/opp_continuous/contNf.
 apply: segment_inc_surj_continuous.
@@ -336,42 +380,45 @@ Qed.
 
 Lemma segment_mono_surj_continuous a b f :
     monotonous `[a, b] f -> set_surj `[a, b] (f @`[a, b]) f ->
-  {in `]a, b[, continuous f}.
+  {within `[a, b], continuous f}.
 Proof.
-move=> -[fle|fge] f_surj x xab; have leab : a <= b by rewrite (itvP xab).
+rewrite continuous_subspace_in => -[fle|fge] f_surj x /set_mem /= xab.
+  have leab : a <= b by rewrite (itvP xab).
   have fafb : f a <= f b by rewrite fle // ?bound_itvE.
-  by apply: segment_inc_surj_continuous x xab => //; case: ltrP f_surj fafb.
+  by apply: segment_inc_surj_continuous => //; case: ltrP f_surj fafb.
+have leab : a <= b by rewrite (itvP xab).
 have fafb : f b <= f a by rewrite fge // ?bound_itvE.
-by apply: segment_dec_surj_continuous x xab => //; case: ltrP f_surj fafb.
+by apply: segment_dec_surj_continuous => //; case: ltrP f_surj fafb.
 Qed.
 
-
 Lemma segment_can_le_continuous a b f g : a <= b ->
-  {in `[a, b], continuous f} ->
+  {within `[a, b], continuous f} ->
   {in `[a, b], cancel f g} ->
-  {in `](f a), (f b)[, continuous g}.
+  {within `[(f a), (f b)], continuous g}.
 Proof.
-move=> aLb ctf fK x xab; have faLfb : f a <= f b by rewrite (itvP xab).
-apply: segment_inc_surj_continuous x xab; first exact: segment_can_le.
+move=> aLb ctf; rewrite continuous_subspace_in => fK x /set_mem /= xab.
+have faLfb : f a <= f b by rewrite (itvP xab).
+apply: segment_inc_surj_continuous; first exact: segment_can_le.
 rewrite !fK ?bound_itvE//=; apply: (@can_surj _ _ f); first by rewrite mem_setE.
 exact/image_subP/mem_inc_segment/segment_continuous_inj_le/(can_in_inj fK).
 Qed.
 
 Lemma segment_can_ge_continuous a b f g : a <= b ->
-  {in `[a, b], continuous f} ->
+  {within `[a, b], continuous f} ->
   {in `[a, b], cancel f g} ->
-  {in `](f b), (f a)[, continuous g}.
+  {within `[(f b), (f a)], continuous g}.
 Proof.
-move=> aLb ctf fK x xab; have fbLfa : f b <= f a by rewrite (itvP xab).
-apply: segment_dec_surj_continuous x xab; first exact: segment_can_ge.
+move=> aLb ctf; rewrite continuous_subspace_in => fK x /set_mem /= xab.
+have fbLfa : f b <= f a by rewrite (itvP xab).
+apply: segment_dec_surj_continuous; first exact: segment_can_ge.
 rewrite !fK ?bound_itvE//=; apply: (@can_surj _ _ f); first by rewrite mem_setE.
 exact/image_subP/mem_dec_segment/segment_continuous_inj_ge/(can_in_inj fK).
 Qed.
 
 Lemma segment_can_continuous a b f g : a <= b ->
-  {in `[a, b], continuous f} ->
+  {within `[a, b], continuous f} ->
   {in `[a, b], cancel f g} ->
-  {in f @`]a, b[, continuous g}.
+  {within f @`[a, b], continuous g}.
 Proof.
 move=> aLb crf fK x; case: lerP => // _;
   by [apply: segment_can_ge_continuous|apply: segment_can_le_continuous].
@@ -386,17 +433,26 @@ have e_gt0 : 0 < e by near: e; exists 1 => /=.
 have xBeLxDe : x - e <= x + e by rewrite ler_add2l gt0_cp.
 have fcte : {in `[x - e, x + e], continuous f}.
   by near: e; apply/at_right_in_segment.
+have fwcte : {within `[x - e, x + e], continuous f}.
+  apply: continuous_in_subspaceT => y yI.
+  by apply: fcte; move/set_mem: yI.
 have fKe : {in `[x - e, x + e], cancel f g}
   by near: e; apply/at_right_in_segment.
 have nearfx : \forall y \near f x, y \in f @`](x - e), (x + e)[.
   apply: near_in_itv; apply: mono_mem_image_itvoo; last first.
     by rewrite in_itv/= -ltr_distlC subrr normr0.
-  apply: itv_continuous_inj_mono; first by near: e; apply/at_right_in_segment.
+  apply: itv_continuous_inj_mono; first exact: fwcte.
   by apply: (@can_in_inj _ _ _ _ g); near: e; apply/at_right_in_segment.
-split; near=> y.
-  by apply: (@segment_can_continuous (x - e) (x + e) f) => //; near: y.
-rewrite (@segment_continuous_can_sym (x - e) (x + e))//.
-by apply: subset_itv_oo_cc; near: y.
+have fxI : f x \in f @`]x - e, x + e[ by exact: (nbhs_singleton nearfx).
+split; near=> y; first last.
+  rewrite (@segment_continuous_can_sym (x - e) (x + e))//.
+  by apply: subset_itv_oo_cc; near: y.
+near: y; apply: (filter_app _ _ nearfx); near_simpl; near=> y => yfe.
+have : {within f @`]x - e, (x + e)[, continuous g}.
+  apply: continuous_subspaceW; last exact: (segment_can_continuous _ fwcte _).
+  exact: subset_itv_oo_cc.
+rewrite continuous_open_subspace; first by (apply;exact: mem_set).
+exact: interval_open.
 Unshelve. all: by end_near. Qed.
 
 Lemma near_can_continuous f g (x : R) :
@@ -429,11 +485,13 @@ move=> x; case: (ltrgtP x 0) => [xlt0 | xgt0 | ->].
   near=> z; rewrite subr0 /=; apply: ltr0_sqrtr.
   rewrite -(opprK x) subr_lt0; apply: ltr_normlW.
   by near: z; apply: nbhs0_lt; rewrite ltr_oppr oppr0.
-- suff main b : 0 <= b -> {in `]0 ^+ 2, (b ^+ 2)[, continuous (@Num.sqrt R)}.
-    apply: (@main (x + 1)); rewrite ?ler_paddl// ?in_itv/= ?ltW// expr0n xgt0/=.
+- suff main b : 0 <= b -> {in [set` `]0 ^+ 2, (b ^+ 2)[], continuous (@Num.sqrt R)}.
+    apply: (@main (x + 1)); rewrite ?ler_paddl // ?mem_setE ?in_itv/= ?ltW// expr0n xgt0/=.
     by rewrite sqrrD1 ltr_paddr// ltr_paddl ?sqr_ge0// (ltr_pmuln2l _ 1%N 2%N).
-  move=> b0; apply: (@segment_can_le_continuous _ _ _ (@GRing.exp _^~ _)) => //.
-    by apply: in1W; apply: exprn_continuous.
+  move=> b0; rewrite -continuous_open_subspace; last exact: interval_open.
+  apply: continuous_subspaceW; first exact: subset_itv_oo_cc.
+  apply: (@segment_can_le_continuous _ _ _ (@GRing.exp _^~ _)) => //.
+    by apply: continuous_subspaceT; exact: exprn_continuous.
   by move=> y y0b; rewrite sqrtr_sqr ger0_norm// (itvP y0b).
 - apply/cvg_distP => _ /posnumP[e]; rewrite !near_simpl /=; near=> y.
   rewrite sqrtr0 sub0r normrN ger0_norm ?sqrtr_ge0 //.
diff --git a/theories/topology.v b/theories/topology.v
index 1d5edbd0b6..5e815471d0 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -5375,20 +5375,14 @@ Notation "{ 'uniform`' A -> V }" := (@fct_RestrictedUniform _ A V) :
 Notation "{ 'uniform' U -> V }" := ({uniform` (@setT U) -> V}) :
   classical_set_scope.
 
-Definition uniform_fun {U : choiceType} A (V : uniformType)
-  (f : U -> V) : {uniform` A -> V} := f.
-Arguments uniform_fun : simpl never.
-
-Notation "{ 'uniform' A , F --> f }" :=
-  (F --> f : @fct_RestrictedUniform _ A _)
-  (only printing) : classical_set_scope.
-Notation "{ 'uniform' , F --> f }" :=
-  (F --> f : @fct_RestrictedUniform _ setT _)
-  (only printing) : classical_set_scope.
 Notation "{ 'uniform' A , F --> f }" :=
-  (F --> uniform_fun A f) : classical_set_scope.
+  (cvg_to [filter of F] 
+     (filter_of (Phantom (fct_RestrictedUniform A) f)))
+   : classical_set_scope.
 Notation "{ 'uniform' , F --> f }" :=
-  (F --> uniform_fun setT f) : classical_set_scope.
+  (cvg_to [filter of F] 
+     (filter_of (Phantom (fct_RestrictedUniform setT) f)))
+   : classical_set_scope.
 
 (* We use this function to help coq identify the correct notation to use
    when printing. Otherwise you get goals like `F --> f -> F --> f`      *)
@@ -5414,14 +5408,10 @@ Canonical fct_PointwiseTopologicalType (U : Type) (V : topologicalType) :=
      @fct_PointwiseTopology U V].
 
 Notation "{ 'ptws' U -> V }" := (@fct_Pointwise U V).
-Definition pointwise_fun {U : Type} {V : topologicalType}
-  (f : U -> V) : {ptws U -> V} := f.
 
 Notation "{ 'ptws' , F --> f }" :=
-  (F --> (f : @fct_Pointwise _ _))
-  (only printing) : classical_set_scope.
-Notation "{ 'ptws' , F --> f }" :=
-  (F --> @pointwise_fun _ _ f) : classical_set_scope.
+  (cvg_to [filter of F] (filter_of (Phantom (@fct_Pointwise _ _) f)))
+  : classical_set_scope.
 
 Lemma pointwise_cvgE {U : Type} {V : topologicalType}
     (F : set (set(U -> V))) (A : set U) (f : U -> V) :
@@ -5436,9 +5426,9 @@ Lemma uniform_set1 F (f : U -> V) (x : U) :
 Proof.
 move=> FF; rewrite propeqE; split.
   move=> + W => /(_ [set t | W (t x)]) +; rewrite /filter_of -nbhs_entourageE.
-  rewrite /uniform_fun uniform_nbhs => + [Q entQ subW].
+  rewrite uniform_nbhs => + [Q entQ subW].
   by apply; exists Q; split => // h Qf; exact/subW/Qf.
-move=> Ff W; rewrite /filter_of uniform_nbhs /uniform_fun => [[E] [entE subW]].
+move=> Ff W; rewrite /filter_of uniform_nbhs => [[E] [entE subW]].
 apply: (filterS subW); move/(nbhs_entourage (f x))/Ff: entE => //=; near_simpl.
 by apply: filter_app; apply: nearW=> ? ? ? ->.
 Qed.
@@ -5454,7 +5444,7 @@ Qed.
 Lemma uniform_subset_cvg (f : U -> V) (A B : set U) F :
   Filter F -> B `<=` A -> {uniform A, F --> f} -> {uniform B, F --> f}.
 Proof.
-move => FF /uniform_subset_nbhs => /(_ f); rewrite /uniform_fun.
+move => FF /uniform_subset_nbhs => /(_ f). 
 by move=> nbhsF Acvg; apply: cvg_trans; [exact: Acvg|exact: nbhsF].
 Qed.
 
@@ -5462,7 +5452,7 @@ Lemma pointwise_uniform_cvg  (f : U -> V) (F : set (set (U -> V))) :
   Filter F -> {uniform, F --> f} -> {ptws, F --> f}.
 Proof.
 move=> FF; rewrite cvg_sup => + i; have isubT : [set i] `<=` setT by move=> ?.
-move=> /(uniform_subset_cvg _ isubT); rewrite /pointwise_fun uniform_set1.
+move=> /(uniform_subset_cvg _ isubT); rewrite uniform_set1.
 rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v).
 apply: cvg_trans => W /=; rewrite nbhs_simpl; exists (@^~ i @^-1` W) => //.
 by rewrite image_preimage // eqEsubset; split=> // j _; exists (fun _ => j).
@@ -5512,8 +5502,7 @@ Lemma uniform_restrict_cvg
   {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
 Proof.
 move=> FF; rewrite cvg_sigL; split.
-- rewrite -sigLK /uniform_fun.
-  move /(cvg_app valL) => D.
+- rewrite -sigLK; move/(cvg_app valL) => D.
   apply: cvg_trans; first exact: D.
   move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
   apply/uniform_nbhs; exists E; split=> //= h /=.
@@ -5524,7 +5513,7 @@ move=> FF; rewrite cvg_sigL; split.
   apply: cvg_trans; first exact: D.
   move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
   apply/uniform_nbhs; exists E; split=> //= h /=.
-  rewrite /sigL /uniform_fun => R [u Au] _ /=.
+  rewrite /sigL => R [u Au] _ /=.
   by have := R u I; rewrite /patch Au.
 Qed.
 
@@ -5533,7 +5522,7 @@ Lemma cvg_uniformU (f : U -> V) (F : set (set (U -> V))) A B : Filter F ->
   {uniform (A `|` B), F --> f}.
 Proof.
 move=> FF AFf BFf Q /=/uniform_nbhs [E [entE EsubQ]].
-apply: (filterS EsubQ); rewrite /uniform_fun.
+apply: (filterS EsubQ).
 rewrite (_:  [set h | (forall y : U, (A `|` B) y -> E (f y, h y))] =
     [set h | forall y, A y -> E (f y, h y)] `&`
     [set h | forall y, B y -> E (f y, h y)]).
@@ -5561,9 +5550,6 @@ Definition family_cvg_uniformType (fam: set U -> Prop) :=
     (sigT fam) 
     (fun k => Uniform.class (@fct_restrictedUniformType U (projT1 k) V)).
 
-Definition restrict_fam fam (f : U -> V) : fct_UniformFamily fam := f.
-Arguments restrict_fam : simpl never.
-
 Canonical fct_UniformFamilyFilteredType fam :=
   [filteredType fct_UniformFamily fam of
     fct_UniformFamily fam for
@@ -5580,7 +5566,8 @@ Canonical fct_UniformFamilyUniformType fam :=
      family_cvg_uniformType fam].
 
 Local Notation "{ 'family' fam , F --> f }" :=
-  (F --> restrict_fam fam f) : classical_set_scope.
+  (cvg_to [filter of F] (filter_of (Phantom (fct_UniformFamily fam) f)))
+  : classical_set_scope.
 
 Lemma fam_cvgP (fam : set U -> Prop) (F : set (set (U -> V))) (f : U -> V) :
   Filter F -> {family fam, F --> f} <->
@@ -5618,7 +5605,8 @@ End UniformCvgLemmas.
 
 Notation "{ 'family' fam , U -> V }" :=  (@fct_UniformFamily U V fam).
 Notation "{ 'family' fam , F --> f }" :=
-  (F --> restrict_fam fam f) : classical_set_scope.
+  (cvg_to [filter of F] (filter_of (Phantom (fct_UniformFamily fam) f)))
+  : classical_set_scope.
 
 Lemma fam_cvgE {U : choiceType} {V : uniformType} (F : set (set (U -> V)))
     (f : U -> V) fam :
@@ -5932,8 +5920,11 @@ Global Instance subspace_proper_filter {T : topologicalType}
      (A : set T) (x : subspace A) :
    ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x.
 
-Notation "{ 'within' A , 'continuous' f }" :=
-  (continuous (f : subspace A -> _)).
+(*Notation "{ 'within' A , 'continuous' f }" :=
+  (continuous (f : subspace A -> _)).*)
+Notation "{ 'within' A , 'continuous' f }" := (forall x,
+  cvg_to [filter of fmap f (filter_of (Phantom (subspace A) x))]
+         [filter of f x]).
 
 Section SubspaceRelative.
 Context {T : topologicalType}.
@@ -6026,6 +6017,21 @@ rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //.
 - by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS.
 Qed.
 
+
+Lemma continuous_subspace0 {U} (f : T -> U) : {within set0, continuous f}.
+Proof.
+move=> x Q; rewrite nbhs_simpl /= {2}/nbhs /=.
+by case: (nbhs_subspaceP (@set0 T) x) => // _ /nbhs_singleton /= ? ? ->.
+Qed.
+
+Lemma continuous_subspace1 {U} (a : T) (f : T -> U) :
+  {within [set a], continuous f}.
+Proof.
+move=> x Q; rewrite nbhs_simpl /= {2}/nbhs /=.
+case: (nbhs_subspaceP [set a] x); last by move=> _ /nbhs_singleton /= ? ? ->.
+by move=> -> /nbhs_singleton ?; apply: nearW => ? ->.
+Qed.
+
 End SubspaceRelative.
 
 Section SubspaceUniform.
@@ -6264,7 +6270,7 @@ Definition singletons {T : Type} := [set [set x] | x in @setT T].
 Lemma pointwise_cvg_family_singleton F (f: U -> V):
   Filter F -> {ptws, F --> f} = {family @singletons U, F --> f}.
 Proof.
-move=> FF; rewrite propeqE fam_cvgP cvg_sup /pointwise_fun; split.
+move=> FF; rewrite propeqE fam_cvgP cvg_sup; split.
   move=> + A [x _ <-] => /(_ x); rewrite uniform_set1.
   rewrite cvg_image; last by rewrite eqEsubset; split=> v // _; exists (cst v).
   apply: cvg_trans => W /=; rewrite ?nbhs_simpl /fmap /= => [[W' + <-]].