add continuous_within_itvcyP/ycP (#1376)

* add continuous_within_itvcNyP/ycP

---------

Co-authored-by: Reynald Affeldt <[email protected]>

Author: IshiguroYoshihiro

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,12 @@
 
 ### Added
 
+- in `num_topology.v`:
+  + lemma `in_continuous_mksetP`
+
+- in `normedtype.v`:
+  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
+
 ### Changed
 
 ### Renamed

theories/normedtype.v

@@ -8,7 +8,6 @@ From mathcomp Require Import cardinality set_interval ereal reals.
 From mathcomp Require Import signed topology prodnormedzmodule function_spaces.
 From mathcomp Require Export real_interval separation_axioms tvs.
 
-
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
 (*                                                                            *)
@@ -2158,31 +2157,58 @@ 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 ->
+Section continuous_within_itvP.
+Context {R : realType}.
+Implicit Type f : R -> R.
+
+Let near_at_left (a : itv_bound R) b f eps : (a < BLeft b)%O -> 0 < eps ->
+  {within [set` Interval a (BRight b)], continuous f} ->
+  \forall t \near b^'-, normr (f b - f t) < eps.
+Proof.
+move=> ab eps_gt0 cf.
+move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (cf b).
+rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
+rewrite -nbhs_subspace_in//; last first.
+  rewrite /= in_itv/= lexx andbT.
+  by move: a ab {cf} => [[a|a]/=|[|]//]; rewrite bnd_simp// => /ltW.
+rewrite /within/= near_simpl; apply: filter_app.
+move: a ab {cf} => [a0 a/= /[!bnd_simp] ab|[_|//]].
+- exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+  apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
+  rewrite gtr0_norm ?subr_gt0// ltrD2l ltrNr opprK => {}ac.
+  by case: a0 => //=; exact/ltW.
+- by exists 1%R => //= c cb1 + bc; apply; rewrite ?lt_eqF ?in_itv/= ?ltW.
+Qed.
+
+Let near_at_right a (b : itv_bound R) f eps : (BRight a < b)%O -> 0 < eps ->
+  {within [set` Interval (BLeft a) b], continuous f} ->
+  \forall t \near a^'+, normr (f a - f t) < eps.
+Proof.
+move=> ab eps_gt0 cf.
+move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (cf a).
+rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=.
+rewrite -nbhs_subspace_in//; last first.
+  rewrite /= in_itv/= lexx//=.
+  by move: b ab {cf} => [[b|b]/=|[|]//]; rewrite bnd_simp// => /ltW.
+rewrite /within/= near_simpl; apply: filter_app.
+move: b ab {cf} => [b0 b/= /[!bnd_simp] ab|[//|_]].
+- exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
+  apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
+  rewrite ltr0_norm ?subr_lt0// opprB ltrD2r.
+  by case: b0 => //= /ltW.
+- by exists 2%R => //= c ca1 + ac; apply; rewrite ?gt_eqF ?in_itv/= ?ltW.
+Qed.
+
+Lemma continuous_within_itvP a b f : a < b ->
   {within `[a, b], continuous f} <->
   [/\ {in `]a, b[, continuous f}, f @ a^'+ --> f a & f @b^'- --> f b].
 Proof.
 move=> ab; split=> [abf|].
-  have [aab bab] : a \in `[a, b] /\ b \in `[a, b].
-    by rewrite !in_itv/= !lexx (ltW ab).
-  split; [|apply/cvgrPdist_lt => eps eps_gt0 /=..].
-  - suff : {in `]a, b[%classic, continuous f}.
-      by move=> P c W; apply: P; rewrite inE.
-    rewrite -continuous_open_subspace; last exact: interval_open.
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=..].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
     by move: abf; exact/continuous_subspaceW/subset_itvW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a).
-    rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
-    apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=.
-    by rewrite ltr0_norm ?subr_lt0// opprB ltrD2r => /ltW.
-  - move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b).
-    rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=.
-    rewrite -nbhs_subspace_in// /within/= near_simpl.
-    apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac.
-    apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=.
-    by rewrite gtr0_norm ?subr_gt0// ltrD2l ltrNr opprK => /ltW.
+  - by apply: near_at_right => //; rewrite bnd_simp.
+  - by apply: near_at_left => //; rewrite bnd_simp.
 case=> ctsoo ctsL ctsR; apply/subspace_continuousP => x /andP[].
 rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
 - by move/eqP; rewrite lt_eqF.
@@ -2202,6 +2228,52 @@ rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|].
   by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open].
 Qed.
 
+Lemma continuous_within_itvcyP a (f : R -> R) :
+  {within `[a, +oo[, continuous f} <->
+  {in `]a, +oo[, continuous f} /\ f x @[x --> a^'+] --> f a.
+Proof.
+split=> [cf|].
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
+    by apply: continuous_subspaceW cf => ?; rewrite /= !in_itv !andbT/= => /ltW.
+  - by apply: near_at_right => //; rewrite bnd_simp.
+move=> [cf fa]; apply/subspace_continuousP => x /andP[].
+rewrite bnd_simp/= le_eqVlt => /predU1P[<-{x}|ax] _.
+- apply/cvgrPdist_lt => eps eps_gt0/=; move/cvgrPdist_lt/(_ _ eps_gt0) : fa.
+  rewrite /at_right !near_withinE; apply: filter_app.
+  exists 1%R => //= c c1a /[swap]; rewrite in_itv/= andbT le_eqVlt.
+  by move=> /predU1P[->|/[swap]/[apply]//]; rewrite subrr normr0.
+- have xaoo : x \in `]a, +oo[ by rewrite in_itv/= andbT.
+  rewrite within_interior; first exact: cf.
+  suff : `]a, +oo[ `<=` interior `[a, +oo[ by exact.
+  rewrite -open_subsetE; last exact: interval_open.
+  by move=> ?/=; rewrite !in_itv/= !andbT; exact: ltW.
+Qed.
+
+Lemma continuous_within_itvNycP b (f : R -> R) :
+  {within `]-oo, b], continuous f} <->
+  {in `]-oo, b[, continuous f} /\ f x @[x --> b^'-] --> f b.
+Proof.
+split=> [cf|].
+  split; [apply/in_continuous_mksetP|apply/cvgrPdist_lt => eps eps_gt0 /=].
+  - rewrite -continuous_open_subspace; last exact: interval_open.
+    by apply: continuous_subspaceW cf => ?/=; rewrite !in_itv/=; exact: ltW.
+  - by apply: near_at_left => //; rewrite bnd_simp.
+move=> [cf fb]; apply/subspace_continuousP => x /andP[_].
+rewrite bnd_simp/= le_eqVlt=> /predU1P[->{x}|xb].
+- apply/cvgrPdist_lt => eps eps_gt0/=; move/cvgrPdist_lt/(_ _ eps_gt0) : fb.
+  rewrite /at_right !near_withinE; apply: filter_app.
+  exists 1%R => //= c c1b /[swap]; rewrite in_itv/= le_eqVlt.
+  by move=> /predU1P[->|/[swap]/[apply]//]; rewrite subrr normr0.
+- have xb_i : x \in `]-oo, b[ by rewrite in_itv/=.
+  rewrite within_interior; first exact: cf.
+  suff : `]-oo, b[ `<=` interior `]-oo, b] by exact.
+  rewrite -open_subsetE; last exact: interval_open.
+  by move=> ?/=; rewrite !in_itv/=; exact: ltW.
+Qed.
+
+End continuous_within_itvP.
+
 Lemma within_continuous_continuous {R : realType} a b (f : R -> R) x : (a < b)%R ->
   {within `[a, b], continuous f} -> x \in `]a, b[ -> {for x, continuous f}.
 Proof.

theories/topology_theory/num_topology.v

@@ -90,6 +90,13 @@ End numFieldTopology.
 
 Import numFieldTopology.Exports.
 
+Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType}
+    (i : interval T) (f : T -> U) :
+  {in i, continuous f} <-> {in [set` i], continuous f}.
+Proof.
+by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE].
+Qed.
+
 Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R ->
  \forall r \near nbhs (0%R:R), (r <= x)%R.
 Proof.