From 86154d7ef80394b703895d6f40df7dedc931c8a9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 26 Sep 2026 01:24:29 +0900 Subject: [PATCH 1/3] unif cont -> cont --- CHANGELOG_UNRELEASED.md | 2 ++ theories/topology_theory/uniform_structure.v | 22 ++++++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 47586cd04c..6d3bc729b0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -11,6 +11,8 @@ + lemma `limn_einf_shift_new` + lemma `limn_einf_shiftS` + lemma `limn_einf_cst` +- in `uniform_structure.v`: + + lemma `unif_continuous_continuous` ### Changed diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index 9169e8af18..b682c4f95a 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -328,6 +328,28 @@ Qed. Definition unif_continuous (U V : uniformType) (f : U -> V) := (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage. +Lemma unif_continuous_continuous (U V : uniformType) (f : U -> V) : + unif_continuous f -> continuous f. +Proof. +move=> ucf /= u N fuN. +have [V0 entV0 V0N] : exists2 V0 : set (V * V), + entourage V0 & xsection V0 (f u) `<=` N. + move: fuN; rewrite -filter_from_entourageE => -[V1 entV1 V1fuN]. + by exists V1. +have [U0 entU0 U0V0] : exists2 U0 : set (U * U), + entourage U0 & (fun x => (f x.1, f x.2)) @` U0 `<=` V0. + exists ((fun x => (f x.1, f x.2)) @^-1` V0). + exact: ucf. + by move=> [_ _]/= [x V0fx [<- <-]]. +have fU0uN : f @` (xsection U0 u) `<=` N. + move=> _/= [u0 U0u0 <-]; apply: V0N => /=. + by apply/mem_set/U0V0 => /=; exists (u, u0) => //=; exact/set_mem. +apply/nbhsP; exists U0 => //. +have := @preimage_subset _ _ f _ _ fU0uN. +apply: subset_trans => u0/= U0uu0. +by exists u0. +Qed. + Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := exists2 B, entourage B & forall PQ, A PQ -> forall p q, PQ.1 p -> PQ.2 q -> B (p,q). From b926f2f207ddac7455441066084f4156f61109ee Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 29 Sep 2026 22:03:15 +0900 Subject: [PATCH 2/3] Co-authored-by: Takafumi Saikawa --- classical/unstable.v | 2 +- theories/topology_theory/uniform_structure.v | 28 +++++++------------- 2 files changed, 11 insertions(+), 19 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 2045878059..7e3c2827f8 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -424,7 +424,7 @@ End reassociate_products. Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1). Proof. by case=> ? ?. Qed. -Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) := +Definition map_pair {S U : Type} (f : S -> U) (x : S * S) : (U * U) := (f x.1, f x.2). Section order_min. diff --git a/theories/topology_theory/uniform_structure.v b/theories/topology_theory/uniform_structure.v index b682c4f95a..caa36a3e54 100644 --- a/theories/topology_theory/uniform_structure.v +++ b/theories/topology_theory/uniform_structure.v @@ -1,6 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import boot order algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import topology_structure. (**md**************************************************************************) @@ -326,28 +328,18 @@ by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhs_entourage. Qed. Definition unif_continuous (U V : uniformType) (f : U -> V) := - (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage. + (map_pair f) @ entourage --> entourage. Lemma unif_continuous_continuous (U V : uniformType) (f : U -> V) : unif_continuous f -> continuous f. Proof. -move=> ucf /= u N fuN. -have [V0 entV0 V0N] : exists2 V0 : set (V * V), - entourage V0 & xsection V0 (f u) `<=` N. - move: fuN; rewrite -filter_from_entourageE => -[V1 entV1 V1fuN]. - by exists V1. -have [U0 entU0 U0V0] : exists2 U0 : set (U * U), - entourage U0 & (fun x => (f x.1, f x.2)) @` U0 `<=` V0. - exists ((fun x => (f x.1, f x.2)) @^-1` V0). - exact: ucf. - by move=> [_ _]/= [x V0fx [<- <-]]. -have fU0uN : f @` (xsection U0 u) `<=` N. - move=> _/= [u0 U0u0 <-]; apply: V0N => /=. - by apply/mem_set/U0V0 => /=; exists (u, u0) => //=; exact/set_mem. -apply/nbhsP; exists U0 => //. -have := @preimage_subset _ _ f _ _ fU0uN. -apply: subset_trans => u0/= U0uu0. -by exists u0. +rewrite /unif_continuous /cvg_to !nbhs_simpl => ucf. +rewrite /cvg_to /= => u X; rewrite !nbhs_simpl /= -!nbhs_entourageE. +case => Y /ucf /=; set Y' := (Y' in entourage Y') => eY' YX. +exists Y' => //. +rewrite /Y' /=. +rewrite -image_sub => v [] u' /= Yfuu' <-. +exact: YX. Qed. Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := From d68873b59e6ba29beaf6121135c778f5bcc16a2b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 29 Sep 2026 22:51:15 +0900 Subject: [PATCH 3/3] fix --- theories/normedtype_theory/tvs.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 79719f209c..fbf94e28f7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -299,7 +299,8 @@ have unif : unif_continuous (fun x => (0, x) : M * M). by rewrite inE/= => -[[[a1 a2] [b1 b2]]]/= /[swap]-[] -> -> <-. move=> /= U /sub_unif_continuous /unif /=. rewrite -comp_preimage/= /comp/= /nbhs/=. -by congr entourage => /=; rewrite eqEsubset; split=> x /=; rewrite !sub0r. +congr entourage => /=; rewrite eqEsubset. +by split=> x; rewrite /map_pair/= !sub0r. Qed. Lemma add_unif_continuous : unif_continuous (fun x : M * M => x.1 + x.2). @@ -311,12 +312,12 @@ have unif: unif_continuous (fun x => (x.1, -x.2) : M * M). ((fun xy => (xy.1.1, xy.2.1, (-xy.1.2, -xy.2.2))) @^-1` (U1 `*` U2))). move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. - by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. + by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). move=> /= U /sub_unif_continuous/unif; rewrite /nbhs/=. rewrite -comp_preimage/=/comp/=. -by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !opprK. +by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !opprK. Qed. HB.instance Definition _ := @@ -339,7 +340,7 @@ apply: (@filterS _ _ entourage_filter ((fun xy => (xy.1.1, xy.2.1, (- xy.1.2, - xy.2.2))) @^-1` (U1 `*` U2))). move=> /= [] [] a1 a2 [] b1 b2/= [] ab1 ab2. have /U12 : (a1, b1, (-a2, -b2)) \in U1 `*` U2 by rewrite !inE. - by rewrite inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. + by rewrite /map_pair inE/= => [] [] [] [] c1 c2 [] d1 d2/= cd [] <- <- <- <-. exists (U1, ((fun xy : M * M => (- xy.1, - xy.2)) @^-1` U2)); first by split. by move=> /= [] [] a1 a2 [] b1 b2/= [] aU bU; exists (a1, b1, (a2, b2)). Qed. @@ -374,11 +375,11 @@ have unif: unif_continuous (fun x => (-1, x) : R^o * M). have /U12 : ((-1, -1), x) \in U1 `*` U2. rewrite in_setX/= (mem_set xU2) andbT. by apply/mem_set; exact: entourage_refl. - by rewrite inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. + by rewrite /map_pair inE/= => [[[]]] [] a1 a2 [] b1 b2/= abU [] {2}<- <- <-/=. move=> /= U /scale_unif_continuous/unif/=. rewrite /nbhs/=. rewrite -comp_preimage/=/comp/=. -by congr entourage; rewrite eqEsubset; split=> x /=; rewrite !scaleN1r. +by congr entourage; rewrite eqEsubset; split=> x /=; rewrite /map_pair !scaleN1r. Qed. #[warning="-HB.no-new-instance"]