From 7079af7a86236c4064a0974709e6de607eae72a7 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 15 Aug 2026 15:52:15 +0900 Subject: [PATCH 1/3] generalize continuou_comp_cvg --- CHANGELOG_UNRELEASED.md | 3 +++ theories/ftc.v | 8 ++++++-- .../pseudometric_normed_Zmodule.v | 14 -------------- theories/topology_theory/topology_structure.v | 16 ++++++++++++++++ 4 files changed, 25 insertions(+), 16 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e67c01c12a..f68071480a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -84,6 +84,9 @@ - in `esum.v`: + lemmma `le_esum` +- from `pseudometric_structure.v` to `topology_structure.v` + + lemma `continuous_comp_cvg` + ### Deprecated ### Removed diff --git a/theories/ftc.v b/theories/ftc.v index 25a17f2d0e..eb76e67031 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1857,8 +1857,12 @@ rewrite onemK onem1 => -> //; last 1 first. split => /=. - by move=> x xr1; exact: derivableB. - apply: cvg_at_right_filter; rewrite onemK. - apply: (@continuous_comp_cvg _ _ _ _ onem)=> //=. - by move=> x; apply: continuousB => //; exact: cst_continuous. + apply/continuous_comp_cvg => /=. + apply: continuousB; [exact: cst_continuous |]. + by []. + (* NB: proof search for `{for _, continuous id}` is slow! + But there is no explicit lemma like `id_continuous`. + See Section `continuous_id` in `topology_structure.v`. *) by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id. - by apply: cvg_at_left_filter; exact: cvgB. Qed. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index b1f779a5dc..eebe519432 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -850,20 +850,6 @@ Arguments cvgr_neq0 {R V T F FF f}. #[global] Hint Extern 0 (ProperFilter _^'+) => (apply: at_right_proper_filter) : typeclass_instances. -Lemma continuous_comp_cvg {R : numFieldType} (U V : pseudoMetricNormedZmodType R) - (f : U -> V) (g : R -> U) (r : R) (l : V) : continuous f -> - (f \o g) x @[x --> r] --> l -> f x @[x --> g r] --> l. -Proof. -move=> cf fgl; apply/(@cvgrPdist_le _ V) => /= e e0. -have e20 : 0 < e / 2 by rewrite divr_gt0. -move/(@cvgrPdist_le _ V) : fgl => /(_ _ e20) fgl. -have /(@cvgrPdist_le _ V) /(_ _ e20) fgf := cf (g r). -rewrite !near_simpl/=; near=> t. -rewrite -(@subrK _ (f (g r)) l) -(addrA (_ + _)) (le_trans (ler_normD _ _))//. -rewrite (splitr e) lerD//; last by near: t. -by case: fgl => d /= d0; apply; rewrite /ball_/= subrr normr0. -Unshelve. all: by end_near. Qed. - Section closure_left_right_open. Variable R : realFieldType. Implicit Types z : R. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 7c81842e14..ccc157a970 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -319,6 +319,22 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (cvg_comp _ (fun x => h x.1 x.2) (cvg_pair fa fb)). Qed. +Lemma continuous_comp_cvg (T V U : topologicalType) + (f : T -> V) (h : V -> U) (r : T) (l : U) : + {for f r, continuous h} -> + (h \o f) x @[x --> r] --> l -> h x @[x --> f r] --> l. +move=> cf fgl X. +rewrite nbhsE; case=> Y [] oY Yl YX. +apply/(filterS YX)/cf. +rewrite nbhsE; exists Y => //; split => //. +have := fgl Y. +have : nbhs l Y by rewrite nbhsE; exists Y. +move/[swap]/[apply]. +rewrite nbhsE; case=> W/= [] oW Wr. +rewrite -image_sub/= => /(_ (h (f r))); apply. +by exists r. +Qed. + Lemma cvg_near_cst (T : Type) (U : topologicalType) (l : U) (f : T -> U) (F : set_system T) {FF : Filter F} : (\forall x \near F, f x = l) -> f @ F --> l. From 69b8445333cc25e81a592e8bb0d34230f1009492 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 15 Aug 2026 16:06:57 +0900 Subject: [PATCH 2/3] fix changelog --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f68071480a..20c1050b1a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -84,7 +84,7 @@ - in `esum.v`: + lemmma `le_esum` -- from `pseudometric_structure.v` to `topology_structure.v` +- from `pseudometric_normed_Zmodule.v` to `topology_structure.v` + lemma `continuous_comp_cvg` ### Deprecated From 5447b000c4a3bfdbf74930ebe2d9ce23e09a6491 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 16 Aug 2026 00:06:37 +0900 Subject: [PATCH 3/3] add id_continuous, simplification --- CHANGELOG_UNRELEASED.md | 5 +++- theories/ftc.v | 6 +--- theories/topology_theory/topology_structure.v | 28 ++++++++----------- 3 files changed, 17 insertions(+), 22 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20c1050b1a..80d834bbe2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -41,6 +41,9 @@ + `elementary_functions/trigonometry_functions.v` + `elementary_functions/trigonometry_integral.v` +- in `topology_structure.v`: + + lemma `id_continuous` + ### Changed - in `derive.v`: @@ -84,7 +87,7 @@ - in `esum.v`: + lemmma `le_esum` -- from `pseudometric_normed_Zmodule.v` to `topology_structure.v` +- from `pseudometric_normed_Zmodule.v` to `topology_structure.v`: + lemma `continuous_comp_cvg` ### Deprecated diff --git a/theories/ftc.v b/theories/ftc.v index eb76e67031..7145c6ed5a 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1858,11 +1858,7 @@ split => /=. - by move=> x xr1; exact: derivableB. - apply: cvg_at_right_filter; rewrite onemK. apply/continuous_comp_cvg => /=. - apply: continuousB; [exact: cst_continuous |]. - by []. - (* NB: proof search for `{for _, continuous id}` is slow! - But there is no explicit lemma like `id_continuous`. - See Section `continuous_id` in `topology_structure.v`. *) + by apply: continuousB; [exact: cst_continuous |exact: id_continuous]. by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id. - by apply: cvg_at_left_filter; exact: cvgB. Qed. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index ccc157a970..ca3115f5ec 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -319,20 +319,16 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous). exact: (cvg_comp _ (fun x => h x.1 x.2) (cvg_pair fa fb)). Qed. -Lemma continuous_comp_cvg (T V U : topologicalType) +Lemma continuous_comp_cvg {T V U : topologicalType} (f : T -> V) (h : V -> U) (r : T) (l : U) : {for f r, continuous h} -> (h \o f) x @[x --> r] --> l -> h x @[x --> f r] --> l. -move=> cf fgl X. -rewrite nbhsE; case=> Y [] oY Yl YX. -apply/(filterS YX)/cf. +Proof. +move=> frh hfrl X; rewrite nbhsE => -[Y [oY Yl]]. +move/filterS; apply; apply: frh. rewrite nbhsE; exists Y => //; split => //. -have := fgl Y. -have : nbhs l Y by rewrite nbhsE; exists Y. -move/[swap]/[apply]. -rewrite nbhsE; case=> W/= [] oW Wr. -rewrite -image_sub/= => /(_ (h (f r))); apply. -by exists r. +have /hfrl : nbhs l Y by exact: open_nbhs_nbhs. +by rewrite nbhsE => -[W [oW Wr]]; exact. Qed. Lemma cvg_near_cst (T : Type) (U : topologicalType) @@ -378,6 +374,9 @@ Lemma cst_continuous {T U : topologicalType} (x : U) : continuous (fun _ : T => x). Proof. by move=> t; exact: cvg_cst. Qed. +Lemma id_continuous {T : topologicalType} : continuous (@id T). +Proof. by move=> t; exact: cvg_id. Qed. + Section within_topologicalType. Context {T : topologicalType} (A : set T). Implicit Types B : set T. @@ -1086,8 +1085,8 @@ HB.instance Definition _ {X Y : nbhsType} (f: X -> Y) (f_cts : continuous f) := @isContinuous.Build X Y (mkcts f_cts) f_cts. Section continuous_comp. -Context {X Y Z : topologicalType}. -Context (f : continuousType X Y) (g : continuousType Y Z). +Context {X Y Z : topologicalType} + (f : continuousType X Y) (g : continuousType Y Z). #[local] Lemma cts_fun_comp : continuous (g \o f). Proof. move=> x; apply: continuous_comp; exact: continuous_fun. Qed. @@ -1099,10 +1098,7 @@ End continuous_comp. Section continuous_id. Context {X : topologicalType}. -#[local] Lemma cts_id : continuous (@idfun X). -Proof. by move=> ?. Qed. - -HB.instance Definition _ := @isContinuous.Build X X (@idfun X) cts_id. +HB.instance Definition _ := @isContinuous.Build X X (@idfun X) id_continuous. End continuous_id.