From d6fb6e2908cda1376792768db3b4fe9018db88e2 Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 16:32:06 +0200 Subject: [PATCH 1/4] Subspace continuity lemmas --- theories/normedtype_theory/normed_module.v | 19 +++++++++++++++++++ .../pseudometric_normed_Zmodule.v | 5 +++++ 2 files changed, 24 insertions(+) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1252178b3f..1b4eb77047 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/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`")] @@ -664,6 +670,19 @@ exact: is_cvgMlE_tmp. Qed. End cvg_composition_field. + +Lemma within_continuousM (T : topologicalType) (K : numFieldType) (A : set T) (f g : T -> K) : + {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 (T : topologicalType) (K : numFieldType) (A : set T) (c : K) (f : T -> K) : + {within A, continuous f} -> {within A, continuous (fun=> c) * f}. +Proof. by move=> cf x; apply: cvgMl_tmp; exact: cf. Qed. + +Lemma within_continuousMr (T : topologicalType) (K : numFieldType) (A : set T) (c : K) (f : T -> K) : + {within A, continuous f} -> {within A, continuous f * (fun=> c)}. +Proof. by move=> cf x; apply: cvgMr_tmp; exact: cf. Qed. + #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")] Notation cvgMl := cvgMr_tmp (only parsing). #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")] diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 9f945624de..19f0f20711 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1142,6 +1142,11 @@ 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_continuousN {T : topologicalType} {K : numFieldType} + {V : pseudoMetricNormedZmodType K} (A : set T) (f : T -> V) : + {within A, continuous f} -> {within A, continuous -f}. +Proof. move=> cf x; apply: cvgN; exact: cf. Qed. + Section Closed_Ball. Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R) From cf3bddc8a6b5cb79e6d2314dc4677f06482ab48e Mon Sep 17 00:00:00 2001 From: Arthur Molina-Mounier Date: Wed, 15 Jul 2026 16:32:52 +0200 Subject: [PATCH 2/4] Update changelog --- CHANGELOG_UNRELEASED.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 23a78527d4..0f7c6d1c05 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,6 +234,12 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` +- in file `normed_module.v`, + + new lemmas `within_continuousZ`, `within_continuousM`, + `within_continuousMl`, and `within_continuousMr`. +- in file `pseudometric_normed_Zmodule.v`, + + new lemma `within_continuousN`. + ### Changed - in `realsum.v`: From 52b93c26e3f8e25a5403c5cca73cfd8627f448c3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 19 Jul 2026 22:40:53 +0900 Subject: [PATCH 3/4] nitpicks --- theories/ftc.v | 2 +- theories/normedtype_theory/normed_module.v | 34 +++++++++++++--------- 2 files changed, 21 insertions(+), 15 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index ce2574b049..4920619e1b 100644 --- a/theories/ftc.v +++ b/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. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 1b4eb77047..3756e9508f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -604,8 +604,8 @@ Qed. End cvg_composition_normed. -Lemma within_continuousZ (T : topologicalType) (A : set T) (K : numFieldType) (V : normedModType K) - (k : K) (f : T -> V) : +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. @@ -671,18 +671,6 @@ Qed. End cvg_composition_field. -Lemma within_continuousM (T : topologicalType) (K : numFieldType) (A : set T) (f g : T -> K) : - {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 (T : topologicalType) (K : numFieldType) (A : set T) (c : K) (f : T -> K) : - {within A, continuous f} -> {within A, continuous (fun=> c) * f}. -Proof. by move=> cf x; apply: cvgMl_tmp; exact: cf. Qed. - -Lemma within_continuousMr (T : topologicalType) (K : numFieldType) (A : set T) (c : K) (f : T -> K) : - {within A, continuous f} -> {within A, continuous f * (fun=> c)}. -Proof. by move=> cf x; apply: cvgMr_tmp; exact: cf. Qed. - #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")] Notation cvgMl := cvgMr_tmp (only parsing). #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")] @@ -696,6 +684,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}. From c95e749313f2d63f7493b41428e4a37ec2e8ddae Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 19 Jul 2026 22:44:56 +0900 Subject: [PATCH 4/4] nitpicks --- CHANGELOG_UNRELEASED.md | 8 ++++---- theories/normedtype_theory/normed_module.v | 1 - .../pseudometric_normed_Zmodule.v | 18 +++++++++++------- 3 files changed, 15 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0f7c6d1c05..151cd763d0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -234,11 +234,11 @@ - in `measurable_structure.v`: + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable` -- in file `normed_module.v`, +- in `normed_module.v`, + new lemmas `within_continuousZ`, `within_continuousM`, - `within_continuousMl`, and `within_continuousMr`. -- in file `pseudometric_normed_Zmodule.v`, - + new lemma `within_continuousN`. + `within_continuousMl`, and `within_continuousMr` +- in `pseudometric_normed_Zmodule.v` + + new lemma `within_continuousN` ### Changed diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 3756e9508f..80e2cc4f9d 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -670,7 +670,6 @@ exact: is_cvgMlE_tmp. Qed. End cvg_composition_field. - #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMr_tmp`")] Notation cvgMl := cvgMr_tmp (only parsing). #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `cvgMl_tmp`")] diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 19f0f20711..920f434388 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1130,23 +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 {T : topologicalType} {K : numFieldType} - {V : pseudoMetricNormedZmodType K} (A : set T) (f : T -> V) : - {within A, continuous f} -> {within A, continuous -f}. +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)