lemmas about within-continuity (#1859)

Co-authored-by: @holgerthies

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -50,6 +50,15 @@
   + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`,
     `emeasurable_fun_itv_cc`
 
+- in `subtype_topology.v`:
+  + lemma `within_continuous_comp`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemmas `within_continuousB`, `within_continuousD`
+
+- in `normed_module.v`:
+  + lemma `within_continuous_compN`
+
 ### Changed
 - in `set_interval.v`
   + `itv_is_closed_unbounded` (fix the definition)

theories/normedtype_theory/normed_module.v

@@ -230,6 +230,22 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports.
 End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
+Lemma within_continuous_compN {R : realFieldType} {K : numDomainType}
+    {U : pseudoMetricNormedZmodType K} (f : R -> U) (a b : R) :
+  {within `[- b, - a], continuous f} -> {within `[a, b], continuous f \o -%R}.
+Proof.
+have [ab|ba _ |-> _] := ltgtP a b; last 2 first.
+  by rewrite set_itv_ge ?bnd_simp -?ltNge//; exact: continuous_subspace0.
+  by rewrite set_itv1; exact: continuous_subspace1.
+move/continuous_within_itvP; rewrite ltrN2 => /(_ ab)[cf fb fa].
+apply/(continuous_within_itvP _ ab); split.
+- move=> t tab.
+  apply: (@cvg_comp _ _ _ -%R f); first exact: oppr_continuous.
+  by apply: cf; rewrite oppr_itvoo !opprK.
+- by rewrite -{1}(opprK a); apply/cvg_at_leftNP; exact: fa.
+- by rewrite -{1}(opprK b); apply/cvg_at_rightNP; exact: fb.
+Qed.
+
 Definition pseudoMetric_normed (M : Type) : Type := M.
 
 HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval.
-From mathcomp Require Import archimedean.
+From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
+From mathcomp Require Import interval archimedean.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import set_interval interval_inference ereal reals.
 From mathcomp Require Import topology function_spaces prodnormedzmodule tvs.
@@ -1159,6 +1159,18 @@ 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) :
+  {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) :
+  {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.
+
 Section Closed_Ball.
 
 Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R)

theories/topology_theory/subtype_topology.v

@@ -88,6 +88,17 @@ Proof. exact: (@subspace_valL_continuousP' _ point). Qed.
 
 End subspace_sig.
 
+Lemma within_continuous_comp {U V W : topologicalType}
+  (A : set V) (f : V -> U) (g : U -> W) :
+  {in f @` A, continuous g} ->
+  {within A, continuous f} ->
+  {within A, continuous (g \o f)}.
+Proof.
+move=> cg /subspace_sigL_continuousP cf; apply/subspace_sigL_continuousP.
+rewrite /sigL -compA => /= x; apply: continuous_comp; first exact: cf.
+by apply/cg/image_f; rewrite inE; exact/set_valP.
+Qed.
+
 Section subtype_setX.
 Context {X Y : topologicalType} (A : set X) (B : set Y).