From 44b395a811800d3052334d66b39c5e623f89b3f2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 24 Feb 2026 17:12:42 +0900 Subject: [PATCH 1/4] lemmas about within-continuity --- CHANGELOG_UNRELEASED.md | 5 ++++ .../pseudometric_normed_Zmodule.v | 30 +++++++++++++++++-- 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4aa1cac78..092dffce3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -47,6 +47,11 @@ + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, `emeasurable_fun_itv_cc` +- in `pseudometric_normed_Zmodule.v`: + + lemmas `within_continuousB`, `within_continuousD`, + `within_continuous_comp` + + ### Changed - in set_interval.v + `itv_is_closed_unbounded` (fix the definition) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index bb5d5bdfc..ef9a200f2 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/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,32 @@ 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. + +Lemma within_continuous_comp {U : topologicalType} {R : realFieldType} + (A : set R) (f : R -> U) (g : U -> R) : + {in f @` A, continuous g} -> + {within A, continuous f} -> + {within A, continuous (g \o f)}. +Proof. +move=> cg cf x. +have [xA|xA] := nbhs_subspaceP A x. + apply: cvg_comp; first exact: cf. + exact/cg/image_f/mem_set. +rewrite /continuous_at {2}/nbhs/= -(@nbhs_subspace_out R A x xA). +by move=> B/= [e /= e0 + _ ->]; apply; exact: ballxx. +Qed. + Section Closed_Ball. Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) From a926bd2eaf988148ceaed0a5fe80350cffa4f4e6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 25 Feb 2026 16:28:46 +0900 Subject: [PATCH 2/4] Co-authored-by: @holgerthies --- .../normedtype_theory/pseudometric_normed_Zmodule.v | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index ef9a200f2..eef6ca57a 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1171,18 +1171,15 @@ Lemma within_continuousD {T : topologicalType} {K : numFieldType} {within A, continuous (f + g)}. Proof. by move=> cf cg x; apply: cvgD; [exact: cf|exact: cg]. Qed. -Lemma within_continuous_comp {U : topologicalType} {R : realFieldType} - (A : set R) (f : R -> U) (g : U -> R) : +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 cf x. -have [xA|xA] := nbhs_subspaceP A x. - apply: cvg_comp; first exact: cf. - exact/cg/image_f/mem_set. -rewrite /continuous_at {2}/nbhs/= -(@nbhs_subspace_out R A x xA). -by move=> B/= [e /= e0 + _ ->]; apply; exact: ballxx. +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 Closed_Ball. From 379796cf63860b11cd626c8850cb9cc323f16a79 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 25 Feb 2026 16:48:29 +0900 Subject: [PATCH 3/4] mv earlier in the file hier --- CHANGELOG_UNRELEASED.md | 7 ++++--- .../normedtype_theory/pseudometric_normed_Zmodule.v | 11 ----------- theories/topology_theory/subtype_topology.v | 11 +++++++++++ 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 092dffce3..de7641961 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -47,10 +47,11 @@ + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`, `emeasurable_fun_itv_cc` -- in `pseudometric_normed_Zmodule.v`: - + lemmas `within_continuousB`, `within_continuousD`, - `within_continuous_comp` +- in `subtype_topology.v`: + + lemma `within_continuous_comp` +- in `pseudometric_normed_Zmodule.v`: + + lemmas `within_continuousB`, `within_continuousD` ### Changed - in set_interval.v diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index eef6ca57a..96428cc55 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1171,17 +1171,6 @@ Lemma within_continuousD {T : topologicalType} {K : numFieldType} {within A, continuous (f + g)}. Proof. by move=> cf cg x; apply: cvgD; [exact: cf|exact: cg]. Qed. -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 Closed_Ball. Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index 6b0582264..b9a287d39 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/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). From fd19acba269b7dfb5de4dce877f3b4c1d625d116 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 25 Feb 2026 17:34:34 +0900 Subject: [PATCH 4/4] one more lemma --- CHANGELOG_UNRELEASED.md | 3 +++ theories/normedtype_theory/normed_module.v | 16 ++++++++++++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de7641961..5eb8acf4b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -53,6 +53,9 @@ - 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) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index a564b3525..2fa7e2690 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/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) :=