From 012a3ef93d430c716a4f78ebbe66bcff199ef53e Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Oct 2024 11:55:38 -0400 Subject: [PATCH 1/4] homeomorphims for products --- CHANGELOG_UNRELEASED.md | 5 +++ classical/mathcomp_extra.v | 22 ++++++++++++- theories/topology_theory/product_topology.v | 35 +++++++++++++++++++++ 3 files changed, 61 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 92c340e0d..7b3f64650 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,6 +71,11 @@ + lemma `countable_measurable` - in `realfun.v`: + lemma `cvgr_dnbhsP` + + new definitions `left_assoc_prod`, and `right_assoc_prod`. + + new lemmas `left_assoc_prodK`, `right_assoc_prodK`, and `swapK`. +- in file `product_topology.v`, + + new lemmas `swap_continuous`, `left_assoc_prod_continuous`, and + `right_assoc_prod_continuous`. ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2c72f25ca..d29ca5863 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -18,6 +18,8 @@ From mathcomp Require Import finset interval. (* {in A &, {mono f : x y /~ x <= y}} *) (* sigT_fun f := lifts a family of functions f into a function on *) (* the dependent sum *) +(* left_assoc_prod x := sends (X * Y) * Z to X * (Y * Z) *) +(* right_assoc_prod x := sends X * (Y * Z) to (X * Y) * Z *) (* ``` *) (* *) (******************************************************************************) @@ -373,7 +375,25 @@ Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) : x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e). Proof. by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed. -Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1). +Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1). + +Section reassociate_products. +Context {X Y Z : Type}. +Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) := + (xyz.1.1,(xyz.1.2,xyz.2)). + +Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z := + ((xyz.1,xyz.2.1),xyz.2.2). + +Lemma left_assoc_prodK : cancel left_assoc_prod right_assoc_prod. +Proof. by case;case. Qed. + +Lemma right_assoc_prodK : cancel right_assoc_prod left_assoc_prod. +Proof. by case => ? []. Qed. +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) := (f x.1, f x.2). diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 8e2984d35..f811bd70d 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -231,3 +231,38 @@ by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `compact_setX`")] Notation compact_setM := compact_setX (only parsing). + +Lemma swap_continuous {X Y : topologicalType} : continuous (@swap X Y). +Proof. +case=> a b W /=[[U V]][] /= Ua Vb UVW; exists (V, U); first by split. +by case => //= ? ? [] ? ?; apply: UVW. +Qed. + +Section reassociate_continuous. +Context {X Y Z : topologicalType}. + +Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z). +Proof. +case;case=> a b c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU. +exists ((P `*` Q), R); first split. +- exists (P, Q); first split => //=. + by case=> x y /= [Px Qy]; split => //. +- done. +- case; case=> x y z /= [][] ? ? ?; apply: PVU; split => //. + exact: QRV. +Qed. + +Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z). +Proof. +case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU. +exists (P, (Q `*` R)); first split. +- done. +- exists (Q, R); first split => //=. + by case=> ? ? /= [? ?]; split. +- case=> x [y z] [? [? ?]]; apply: VRU; split => //. + exact: PQV. +Qed. + +End reassociate_continuous. + + From 492465a3bce46b7aaaffec2ae03f1a4cdf2e0eb9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 10 Nov 2024 00:31:34 +0900 Subject: [PATCH 2/4] trailing spaces, nitpicks --- classical/mathcomp_extra.v | 12 ++++---- theories/topology_theory/product_topology.v | 31 +++++++++------------ 2 files changed, 20 insertions(+), 23 deletions(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index d29ca5863..86aaf9a0b 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -379,17 +379,19 @@ Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1). Section reassociate_products. Context {X Y Z : Type}. -Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) := - (xyz.1.1,(xyz.1.2,xyz.2)). -Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z := - ((xyz.1,xyz.2.1),xyz.2.2). +Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) := + (xyz.1.1, (xyz.1.2, xyz.2)). + +Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z := + ((xyz.1, xyz.2.1), xyz.2.2). Lemma left_assoc_prodK : cancel left_assoc_prod right_assoc_prod. -Proof. by case;case. Qed. +Proof. by case; case. Qed. Lemma right_assoc_prodK : cancel right_assoc_prod left_assoc_prod. Proof. by case => ? []. Qed. + End reassociate_products. Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1). diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index f811bd70d..77eab686a 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -234,35 +234,30 @@ Notation compact_setM := compact_setX (only parsing). Lemma swap_continuous {X Y : topologicalType} : continuous (@swap X Y). Proof. -case=> a b W /=[[U V]][] /= Ua Vb UVW; exists (V, U); first by split. -by case => //= ? ? [] ? ?; apply: UVW. +case=> a b W /= [[U V]][] /= Ub Va UVW; exists (V, U); first by split. +by case => //= ? ? [] ? ?; exact: UVW. Qed. Section reassociate_continuous. Context {X Y Z : topologicalType}. -Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z). +Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z). Proof. -case;case=> a b c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU. +move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU. exists ((P `*` Q), R); first split. -- exists (P, Q); first split => //=. - by case=> x y /= [Px Qy]; split => //. -- done. -- case; case=> x y z /= [][] ? ? ?; apply: PVU; split => //. - exact: QRV. +- exists (P, Q); first by []. + by case=> x y /= [Px Qy]. +- by []. +- by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV. Qed. -Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z). +Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z). Proof. case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU. -exists (P, (Q `*` R)); first split. -- done. -- exists (Q, R); first split => //=. - by case=> ? ? /= [? ?]; split. -- case=> x [y z] [? [? ?]]; apply: VRU; split => //. - exact: PQV. +exists (P, (Q `*` R)); first split => //. +- exists (Q, R); first by []. + by case=> ? ? /= []. +- by case=> x [y z] [? [? ?]]; apply: VRU; split => //; exact: PQV. Qed. End reassociate_continuous. - - From 49d896b759666fec3e58b40058e392d786142fa2 Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 9 Nov 2024 14:07:39 -0500 Subject: [PATCH 3/4] more idiomatic naming --- CHANGELOG_UNRELEASED.md | 6 ++++-- classical/mathcomp_extra.v | 12 ++++++------ theories/topology_theory/product_topology.v | 4 ++-- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7b3f64650..174346d49 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -73,9 +73,11 @@ + lemma `cvgr_dnbhsP` + new definitions `left_assoc_prod`, and `right_assoc_prod`. + new lemmas `left_assoc_prodK`, `right_assoc_prodK`, and `swapK`. + + new definitions `prodA`, and `prodAr`. + + new lemmas `prodAK`, `prodArK`, and `swapK`. - in file `product_topology.v`, - + new lemmas `swap_continuous`, `left_assoc_prod_continuous`, and - `right_assoc_prod_continuous`. + + new lemmas `swap_continuous`, `prodA_continuous`, and + `prodAr_continuous`. ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 86aaf9a0b..f0ecf3733 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -18,8 +18,8 @@ From mathcomp Require Import finset interval. (* {in A &, {mono f : x y /~ x <= y}} *) (* sigT_fun f := lifts a family of functions f into a function on *) (* the dependent sum *) -(* left_assoc_prod x := sends (X * Y) * Z to X * (Y * Z) *) -(* right_assoc_prod x := sends X * (Y * Z) to (X * Y) * Z *) +(* prodA x := sends (X * Y) * Z to X * (Y * Z) *) +(* prodAr x := sends X * (Y * Z) to (X * Y) * Z *) (* ``` *) (* *) (******************************************************************************) @@ -380,16 +380,16 @@ Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1). Section reassociate_products. Context {X Y Z : Type}. -Definition left_assoc_prod (xyz : (X * Y) * Z) : X * (Y * Z) := +Definition prodA (xyz : (X * Y) * Z) : X * (Y * Z) := (xyz.1.1, (xyz.1.2, xyz.2)). -Definition right_assoc_prod (xyz : X * (Y * Z)) : (X * Y) * Z := +Definition prodAr (xyz : X * (Y * Z)) : (X * Y) * Z := ((xyz.1, xyz.2.1), xyz.2.2). -Lemma left_assoc_prodK : cancel left_assoc_prod right_assoc_prod. +Lemma prodAK : cancel prodA prodAr. Proof. by case; case. Qed. -Lemma right_assoc_prodK : cancel right_assoc_prod left_assoc_prod. +Lemma prodArK : cancel prodAr prodA. Proof. by case => ? []. Qed. End reassociate_products. diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 77eab686a..4755458fc 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -241,7 +241,7 @@ Qed. Section reassociate_continuous. Context {X Y Z : topologicalType}. -Lemma left_assoc_prod_continuous : continuous (@left_assoc_prod X Y Z). +Lemma prodA_continuous : continuous (@prodA X Y Z). Proof. move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU. exists ((P `*` Q), R); first split. @@ -251,7 +251,7 @@ exists ((P `*` Q), R); first split. - by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV. Qed. -Lemma right_assoc_prod_continuous : continuous (@right_assoc_prod X Y Z). +Lemma prodAr_continuous : continuous (@prodAr X Y Z). Proof. case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU. exists (P, (Q `*` R)); first split => //. From 8dcefbcece551b0f1105c84dcce22a1de8f50f10 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 10 Nov 2024 12:03:19 +0900 Subject: [PATCH 4/4] fix changelog --- CHANGELOG_UNRELEASED.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 174346d49..d48bcd8dc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,8 +71,6 @@ + lemma `countable_measurable` - in `realfun.v`: + lemma `cvgr_dnbhsP` - + new definitions `left_assoc_prod`, and `right_assoc_prod`. - + new lemmas `left_assoc_prodK`, `right_assoc_prodK`, and `swapK`. + new definitions `prodA`, and `prodAr`. + new lemmas `prodAK`, `prodArK`, and `swapK`. - in file `product_topology.v`,