New within_continuous* lemmas

CHANGELOG_UNRELEASED.md

@@ -234,6 +234,12 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in `normed_module.v`,
+  + new lemmas `within_continuousZ`, `within_continuousM`, 
+    `within_continuousMl`, and `within_continuousMr`
+- in `pseudometric_normed_Zmodule.v`
+  + new lemma `within_continuousN`
+
 ### Changed
 
 - in `realsum.v`:

theories/ftc.v

@@ -519,7 +519,7 @@ Let within_continuous_restrict f a b : (a < b)%R ->
 Proof.
 move=> ab + x xab; move=> /(_ x).
 rewrite {1}/continuous_at => xf.
-rewrite /prop_for /continuous_at  patchE.
+rewrite /prop_for /continuous_at patchE.
 rewrite mem_set ?mulr1 /=; first exact: subset_itv_oo_cc.
 exact: cvg_patch.
 Qed.

theories/normedtype_theory/normed_module.v

@@ -603,6 +603,12 @@ by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP.
 Qed.
 
 End cvg_composition_normed.
+
+Lemma within_continuousZ (T : topologicalType) (A : set T) (K : numFieldType)
+    (V : normedModType K) (k : K) (f : T -> V) :
+  {within A, continuous f} -> {within A, continuous k *: f}.
+Proof. by move=> cf x; apply: cvgZl_tmp; exact: cf. Qed.
+
 #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgZr_tmp`")]
 Notation cvgZl := cvgZr_tmp (only parsing).
 #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgZr_tmp`")]
@@ -677,6 +683,24 @@ Notation is_cvgMlE := is_cvgMrE_tmp (only parsing).
 #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `is_cvgMlE_tmp`")]
 Notation is_cvgMrE := is_cvgMlE_tmp (only parsing).
 
+Section within_continuous_lemmas.
+Context {T : topologicalType} {K : numFieldType} (A : set T).
+Implicit Types f g : T -> K.
+
+Lemma within_continuousM f g : {within A, continuous f} ->
+  {within A, continuous g} -> {within A, continuous f * g}.
+Proof. by move=> cf cg x; apply: cvgM; [exact: cf | exact: cg]. Qed.
+
+Lemma within_continuousMl (c : K) f :
+  {within A, continuous f} -> {within A, continuous cst c * f}.
+Proof. by move=> cf x; apply: cvgMl_tmp; exact: cf. Qed.
+
+Lemma within_continuousMr (c : K) f :
+  {within A, continuous f} -> {within A, continuous f * cst c}.
+Proof. by move=> cf x; apply: cvgMr_tmp; exact: cf. Qed.
+
+End within_continuous_lemmas.
+
 Section limit_composition_normed.
 Context {K : numFieldType} {V : normedModType K} {T : Type}.
 Context (F : set_system T) {FF : ProperFilter F}.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1130,18 +1130,27 @@ Proof. by rewrite norm_cvg0P. Qed.
 
 End cvg_composition_pseudometric.
 
-Lemma within_continuousB {T : topologicalType} {K : numFieldType}
-    {V : pseudoMetricNormedZmodType K} (A : set T) (f g : T -> V) :
+Section within_continuous_lemmas.
+Context {T : topologicalType} {K : numFieldType}
+  {V : pseudoMetricNormedZmodType K} (A : set T).
+Implicit Types f g : T -> V.
+
+Lemma within_continuousB f g :
   {within A, continuous f} -> {within A, continuous g} ->
   {within A, continuous (f - g)}.
 Proof. by move=> cf cg x; apply: cvgB; [exact: cf|exact: cg]. Qed.
 
-Lemma within_continuousD {T : topologicalType} {K : numFieldType}
-    {V : pseudoMetricNormedZmodType K} (A : set T) (f g : T -> V) :
+Lemma within_continuousD f g :
   {within A, continuous f} -> {within A, continuous g} ->
   {within A, continuous (f + g)}.
 Proof. by move=> cf cg x; apply: cvgD; [exact: cf|exact: cg]. Qed.
 
+Lemma within_continuousN f :
+  {within A, continuous f} -> {within A, continuous - f}.
+Proof. move=> cf x; apply: cvgN; exact: cf. Qed.
+
+End within_continuous_lemmas.
+
 Section Closed_Ball.
 
 Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R)