filling in admits

theories/normedtype.v

@@ -2904,6 +2904,54 @@ by apply: xe_A => //; rewrite eq_sym.
 Qed.
 Arguments cvg_at_leftE {R V} f x.
 
+Lemma continuous_within_itvP {R : realType } a b (f : R -> R) :
+  a < b ->
+  {within `[a,b], continuous f} <->
+  {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b.
+Proof.
+move=> ab; split.
+have [aab bab] : a \in `[a, b] /\ b \in `[a, b].
+  by split; apply/andP; split => //; apply: ltW.
+have [aabC babC] : `[a, b]%classic a /\ `[a, b]%classic b.
+  by rewrite ?inE /=; split.
+move=> abf; split.
+  suff : {in `]a,b[%classic, continuous f}.
+      by move=> P ? W; by apply: P; move: W; rewrite inE /=.
+    rewrite -(@continuous_open_subspace); last exact: interval_open.
+    by move: abf; apply: continuous_subspaceW; apply: subset_itvW.
+  split; apply/cvgrPdist_lt => eps eps_gt0 /=;
+    [move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a)
+    | move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b)];
+    rewrite /dnbhs /= ?near_withinE ?near_simpl /prop_near1/nbhs /=;
+    rewrite -nbhs_subspace_in // /within /= ?nbhs_simpl near_simpl;
+    apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac;
+    (apply => //; last by apply/eqP => CA; move: ac; rewrite CA ltxx);
+    apply/andP; split; apply: ltW => //; move: cba; rewrite /= ?[(`|a-c|)]distrC ger0_norm. 
+  - by rewrite ltrBlDr -addrA [-_+_]addrC subrr addr0.
+  - by apply: ltW; rewrite subr_gt0.
+  - by rewrite ltrBlDr addrC addrA ltrBrDl -ltrBrDr -addrA subrr addr0. 
+  - by apply: ltW; rewrite subr_gt0.
+case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP [].
+rewrite ?le_eqVlt => /orP + /orP; case => + []. 
+- by move=> /eqP [<-] /eqP [E]; move: ab; rewrite E ltxx.
+- move=> /eqP [<-_]; apply/cvgrPdist_lt => eps eps_gt0 /=.
+  move/cvgrPdist_lt/(_ _ eps_gt0):ctsL; rewrite /at_right ?near_withinE.
+  apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac.
+  (have : a <= c by move: ac => /andP []); rewrite le_eqVlt => /orP [].
+    by move=> /eqP ->; rewrite subrr normr0.
+  by move=> ?; apply.
+- move=> _ /eqP [->]; apply/cvgrPdist_lt => eps eps_gt0 /=.
+  move/cvgrPdist_lt/(_ _ eps_gt0):ctsR; rewrite /at_left ?near_withinE.
+  apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac.
+  (have : c <= b by move: ac => /andP []); rewrite le_eqVlt => /orP [].
+    by move=> /eqP ->; rewrite subrr normr0.
+  by move=> ?; apply.
+- move=> ax xb; have aboox : x \in `]a,b[ by apply/andP; split.
+  rewrite within_interior; first exact: ctsoo.
+  suff : `]a,b[ `<=` interior `[a,b] by apply.
+  rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
+Qed.
+
 (* TODO: generalize to R : numFieldType *)
 Section hausdorff.
 

theories/realfun.v

@@ -1113,6 +1113,7 @@ have : f a >= f b by rewrite (itvP xfafb).
 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 ->
   {within `[a, b], continuous f}.
@@ -1424,12 +1425,7 @@ End is_derive_inverse.
   (eapply is_deriveV; first by []) : typeclass_instances.
 
 From mathcomp Require Import path.
-Require Import sequences.
 
-Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n <= m)%R})
-  (at level 10).
-Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n >= m)%R})
-  (at level 10).
 
 Lemma nondecreasing_funN {R : realType} a b (f : R -> R) :
   {in `[a, b] &, nondecreasing_fun f} <-> {in `[a, b] &, nonincreasing_fun (\- f)}.
@@ -1457,11 +1453,6 @@ Proof.
 by move=> uS [y Sy] /le_trans; apply; apply: sup_ub.
 Qed.
 
-(* NB: already in master? *)
-Lemma ereal_sup_le {R : realType} (S : set (\bar R)) x :
-  (exists2 y, S y & x <= y)%E -> (x <= ereal_sup S)%E.
-Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
-
 Lemma ereal_supy {R : realType} (A : set \bar R) :
   A +oo%E -> ereal_sup A = +oo%E.
 Proof.
@@ -2293,7 +2284,7 @@ Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R).
 Proof. by rewrite /total_variation variations_opp. Qed.
 
 Lemma TV_left_continuous a b x f : a < x -> x <= b ->
-  f @ at_left x --> f x ->
+  f @ x^'- --> f x ->
   BV a b f ->
   fine \o TV a ^~ f @ x^'- --> fine (TV a x f).
 Proof.
@@ -2332,19 +2323,13 @@ apply: (TV_right_continuous _ _ _ bvNf).
 by apply/at_left_at_rightP; rewrite /= opprK.
 Unshelve. all: by end_near. Qed.
 
-Lemma continuous_within_itvP a b (f : R -> R) :
-  {within `[a,b], continuous f} <->
-  {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b.
-Proof.
-Admitted.
-
 Lemma TV_continuous a b (f : R -> R) : a < b ->
   {within `[a,b], continuous f} ->
   BV a b f ->
   {within `[a,b], continuous (fine \o TV a ^~ f)}.
 Proof.
-move=> ab /continuous_within_itvP [int [l r]] bdf.
-apply/continuous_within_itvP; repeat split.
+move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf.
+apply/continuous_within_itvP; (repeat split) => //.
 - move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb].
   apply/left_right_continuousP; split.
     apply: (TV_left_continuous _ (ltW xb)) => //.