homeomorphims for products

CHANGELOG_UNRELEASED.md

@@ -24,6 +24,13 @@
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
 
+- in file `mathcomp_extra.v`,
+  + 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
 
 - in file `normedtype.v`,

classical/mathcomp_extra.v

@@ -13,9 +13,11 @@ From mathcomp Require Import finset interval.
 (*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
 (*                           given x : T i                                    *)
 (*                 swap x := (x.2, x.1)                                       *)
-(*           map_pair f x := (f x.1, f x.2)                                       *)
+(*           map_pair f x := (f x.1, f x.2)                                   *)
 (*         monotonous A f := {in A &, {mono f : x y / x <= y}} \/             *)
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
+(*      left_assoc_prod x := sends (X * Y) * Z to X * (Y * Z)                 *)
+(*     right_assoc_prod x := sends X * (Y * Z) to (X * Y) * Z                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -369,7 +371,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).

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.
+
+