From b4311bcd8148f0b7a8ef49bbd5ea842280dce6f8 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 10 Nov 2024 00:12:47 -0500 Subject: [PATCH 1/3] min and max are continuous --- theories/topology_theory/order_topology.v | 100 +++++++++++++++++++++- 1 file changed, 99 insertions(+), 1 deletion(-) diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index a959bff76..49291cbb5 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. From mathcomp Require Import topology_structure uniform_structure. -From mathcomp Require Import pseudometric_structure. +From mathcomp Require Import product_topology pseudometric_structure. (**md**************************************************************************) (* # Order topology *) @@ -220,3 +220,101 @@ Qed. HB.instance Definition _ := Order_isNbhs.Build _ oT order_nbhs_itv. End induced_order_topology. + +Lemma min_continuous {d} {T : orderTopologicalType d} : + continuous (fun xy : T * T => Order.min xy.1 xy.2). +Proof. +case=> x y; case : (pselect (x = y)). + move=> <- U; rewrite /= min_l // => ux; exists (U, U) => //=. + case=> a b [/= ? ?]; case /orP : (le_total a b) => ?; first by rewrite min_l. + by rewrite min_r. +move=>/eqP; wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP []; first exact: WH. + rewrite eq_sym; move=> yx yNx. + have -> : (fun (xy : T *T ) => Order.min xy.1 xy.2) = + ((fun xy => Order.min xy.1 xy.2) \o @swap T T). + apply/funext; case => a b /=; have /orP [? | ?] := le_total a b. + by rewrite min_l // min_r. + by rewrite min_r // min_l. + apply: continuous_comp; first exact: swap_continuous. + by apply: WH. +move=> _ U /=; (rewrite min_l //; last exact: ltW) => Ux. +case : (pselect (exists z, x < z < y)%O). + case=> z xzy; exists (U `&` `]-oo,z[, `]z,+oo[%classic) => //=. + - split; [apply: filterI =>// |]; apply: open_nbhs_nbhs; split. + + exact: lray_open. + + by rewrite set_itvE; case/andP: xzy. + + exact: rray_open. + + by rewrite set_itvE; case/andP: xzy. + - case=> a b /= [][Ua]; rewrite ?in_itv andbT /= => az ?. + by rewrite min_l //; apply: ltW; apply: (lt_trans az). +move/forallNP => /= xNy. +exists (U `&` `]-oo,y[, `]x,+oo[%classic) => //=. +- split; [apply: filterI =>// |]; apply: open_nbhs_nbhs; split. + + exact: lray_open. + + by rewrite set_itvE. + + exact: rray_open. + + by rewrite set_itvE. +- case=> a b /= [][Ua]; rewrite ?in_itv andbT /= => ay xb. + rewrite min_l //; rewrite leNgt; have := xNy b; apply: contra_notN. + move=> ba; apply/andP; split => //. + by apply: (lt_trans ba). +Qed. + +Lemma min_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} + (f g : X -> T): + continuous f -> continuous g -> continuous (f \min g). +Proof. +move=> fc gc z; apply: continuous2_cvg; first apply min_continuous. + exact: fc. +exact: gc. +Qed. + +Lemma max_continuous {d} {T : orderTopologicalType d} : + continuous (fun xy : T * T => Order.max xy.1 xy.2). +Proof. +case=> x y; case : (pselect (x = y)). + move=> <- U; rewrite /= max_r // => ux; exists (U, U) => //=. + case=> a b [/= ? ?]; case /orP : (le_total a b) => ?; first by rewrite max_r. + by rewrite max_l. +move=>/eqP; wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP []; first exact: WH. + rewrite eq_sym; move=> yx yNx. + have -> : (fun (xy : T *T ) => Order.max xy.1 xy.2) = + ((fun xy => Order.max xy.1 xy.2) \o @swap T T). + apply/funext; case => a b /=; have /orP [? | ?] := le_total a b. + by rewrite max_r // max_l. + by rewrite max_l // max_r. + apply: continuous_comp; first exact: swap_continuous. + by apply: WH. +move=> _ U /=; (rewrite max_r //; last exact: ltW) => Ux. +case : (pselect (exists z, x < z < y)%O). + case=> z xzy; exists (`]-oo,z[%classic, U `&` `]z,+oo[%classic) => //=. + - split; [|apply: filterI =>//]; apply: open_nbhs_nbhs; split. + + exact: lray_open. + + by rewrite set_itvE; case/andP: xzy. + + exact: rray_open. + + by rewrite set_itvE; case/andP: xzy. + - case=> a b /= [] + []; rewrite ?in_itv andbT /= => az ? zb. + by rewrite max_r //; apply: ltW; apply: (lt_trans az). +move/forallNP => /= xNy. +exists (`]-oo,y[%classic, U `&` `]x,+oo[%classic) => //=. +- split; [|apply: filterI =>//]; apply: open_nbhs_nbhs; split. + + exact: lray_open. + + by rewrite set_itvE. + + exact: rray_open. + + by rewrite set_itvE. +- case=> a b /=; rewrite ?in_itv /= andbT => [/=] [ay] [?] xb. + rewrite max_r //; rewrite leNgt; have := xNy b; apply: contra_notN. + move=> ba; apply/andP; split => //. + by apply: (lt_trans ba). +Qed. + +Lemma max_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} + (f g : X -> T): + continuous f -> continuous g -> continuous (f \max g). +Proof. +move=> fc gc z; apply: continuous2_cvg; first apply max_continuous. + exact: fc. +exact: gc. +Qed. From e35a2a5a9bd88ff22e9837cb4fd4a1e97e92f272 Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 10 Nov 2024 00:19:51 -0500 Subject: [PATCH 2/3] adding changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4450c6f19..260152313 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,9 @@ - in `boolp.`: + lemma `existT_inj` +- in file `order_topology.v` + + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and + `max_fun_continuous`. ### Changed From 3512166a98b92b67a51f0e70c1373e7a4178d103 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 10 Nov 2024 22:50:36 +0900 Subject: [PATCH 3/3] linting --- theories/topology_theory/order_topology.v | 136 +++++++++------------- 1 file changed, 57 insertions(+), 79 deletions(-) diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index 49291cbb5..99df6a824 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -224,97 +224,75 @@ End induced_order_topology. Lemma min_continuous {d} {T : orderTopologicalType d} : continuous (fun xy : T * T => Order.min xy.1 xy.2). Proof. -case=> x y; case : (pselect (x = y)). - move=> <- U; rewrite /= min_l // => ux; exists (U, U) => //=. - case=> a b [/= ? ?]; case /orP : (le_total a b) => ?; first by rewrite min_l. - by rewrite min_r. -move=>/eqP; wlog xy : x y / (x < y)%O. - move=> WH /[dup] /lt_total/orP []; first exact: WH. - rewrite eq_sym; move=> yx yNx. - have -> : (fun (xy : T *T ) => Order.min xy.1 xy.2) = - ((fun xy => Order.min xy.1 xy.2) \o @swap T T). - apply/funext; case => a b /=; have /orP [? | ?] := le_total a b. - by rewrite min_l // min_r. - by rewrite min_r // min_l. - apply: continuous_comp; first exact: swap_continuous. - by apply: WH. -move=> _ U /=; (rewrite min_l //; last exact: ltW) => Ux. -case : (pselect (exists z, x < z < y)%O). - case=> z xzy; exists (U `&` `]-oo,z[, `]z,+oo[%classic) => //=. - - split; [apply: filterI =>// |]; apply: open_nbhs_nbhs; split. - + exact: lray_open. - + by rewrite set_itvE; case/andP: xzy. - + exact: rray_open. - + by rewrite set_itvE; case/andP: xzy. - - case=> a b /= [][Ua]; rewrite ?in_itv andbT /= => az ?. - by rewrite min_l //; apply: ltW; apply: (lt_trans az). -move/forallNP => /= xNy. -exists (U `&` `]-oo,y[, `]x,+oo[%classic) => //=. -- split; [apply: filterI =>// |]; apply: open_nbhs_nbhs; split. - + exact: lray_open. - + by rewrite set_itvE. - + exact: rray_open. - + by rewrite set_itvE. -- case=> a b /= [][Ua]; rewrite ?in_itv andbT /= => ay xb. - rewrite min_l //; rewrite leNgt; have := xNy b; apply: contra_notN. - move=> ba; apply/andP; split => //. - by apply: (lt_trans ba). +case=> x y; have [<- U /=|]:= eqVneq x y. + rewrite min_l// => Ux; exists (U, U) => //= -[a b [Ua Ub]]. + by have /orP[?|?]/= := le_total a b; [rewrite min_l|rewrite min_r]. +wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP[|yx /eqP/nesym/eqP yNx]; first exact: WH. + rewrite (_ : (fun _ => _) = (fun xy => Order.min xy.1 xy.2) \o @swap T T). + by apply: continuous_comp; [exact: swap_continuous|exact: WH]. + apply/funext => -[a b/=]; have /orP[ab|ba] := le_total a b. + - by rewrite min_l // min_r. + - by rewrite min_r // min_l. +move=> _ U /=; rewrite (min_l (ltW xy)) => Ux. +have [[z xzy]|/forallNP/= xNy] := pselect (exists z, x < z < y)%O. + exists (U `&` `]-oo, z[, `]z, +oo[%classic) => /=. + split; [apply: filterI =>//|]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy]. + - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy]. + case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => az zb. + by rewrite min_l// (ltW (lt_trans az _)). +exists (U `&` `]-oo, y[, `]x, +oo[%classic) => /=. + split; [apply: filterI => //|]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE]. + - by split; [exact: rray_open|rewrite set_itvE]. +case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => ay xb. +rewrite min_l// leNgt; apply: contra_notN (xNy b) => ba. +by rewrite xb (lt_trans ba). Qed. -Lemma min_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} - (f g : X -> T): +Lemma min_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} + (f g : X -> T) : continuous f -> continuous g -> continuous (f \min g). Proof. -move=> fc gc z; apply: continuous2_cvg; first apply min_continuous. - exact: fc. -exact: gc. +move=> fc gc z; apply: continuous2_cvg; [|exact: fc|exact: gc]. +by apply min_continuous. Qed. Lemma max_continuous {d} {T : orderTopologicalType d} : continuous (fun xy : T * T => Order.max xy.1 xy.2). Proof. -case=> x y; case : (pselect (x = y)). - move=> <- U; rewrite /= max_r // => ux; exists (U, U) => //=. - case=> a b [/= ? ?]; case /orP : (le_total a b) => ?; first by rewrite max_r. - by rewrite max_l. -move=>/eqP; wlog xy : x y / (x < y)%O. - move=> WH /[dup] /lt_total/orP []; first exact: WH. - rewrite eq_sym; move=> yx yNx. - have -> : (fun (xy : T *T ) => Order.max xy.1 xy.2) = - ((fun xy => Order.max xy.1 xy.2) \o @swap T T). - apply/funext; case => a b /=; have /orP [? | ?] := le_total a b. - by rewrite max_r // max_l. - by rewrite max_l // max_r. - apply: continuous_comp; first exact: swap_continuous. - by apply: WH. -move=> _ U /=; (rewrite max_r //; last exact: ltW) => Ux. -case : (pselect (exists z, x < z < y)%O). - case=> z xzy; exists (`]-oo,z[%classic, U `&` `]z,+oo[%classic) => //=. - - split; [|apply: filterI =>//]; apply: open_nbhs_nbhs; split. - + exact: lray_open. - + by rewrite set_itvE; case/andP: xzy. - + exact: rray_open. - + by rewrite set_itvE; case/andP: xzy. - - case=> a b /= [] + []; rewrite ?in_itv andbT /= => az ? zb. - by rewrite max_r //; apply: ltW; apply: (lt_trans az). -move/forallNP => /= xNy. -exists (`]-oo,y[%classic, U `&` `]x,+oo[%classic) => //=. -- split; [|apply: filterI =>//]; apply: open_nbhs_nbhs; split. - + exact: lray_open. - + by rewrite set_itvE. - + exact: rray_open. - + by rewrite set_itvE. -- case=> a b /=; rewrite ?in_itv /= andbT => [/=] [ay] [?] xb. - rewrite max_r //; rewrite leNgt; have := xNy b; apply: contra_notN. - move=> ba; apply/andP; split => //. - by apply: (lt_trans ba). +case=> x y; have [<- U|] := eqVneq x y. + rewrite /= max_r // => ux; exists (U, U) => //= -[a b] [/= Ua Ub]. + by have /orP[?|?]/= := le_total a b; [rewrite max_r|rewrite max_l]. +wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP[|yx /eqP/nesym/eqP yNx]; first exact: WH. + rewrite (_ : (fun _ => _) = (fun xy => Order.max xy.1 xy.2) \o @swap T T). + by apply: continuous_comp; [exact: swap_continuous|exact: WH]. + apply/funext => -[a b] /=; have /orP [ab|ba] := le_total a b. + - by rewrite max_r // max_l. + - by rewrite max_l // max_r. +move=> _ U /=; rewrite (max_r (ltW xy)) => Ux. +have [[z xzy]|/forallNP /= xNy] := pselect (exists z, x < z < y)%O. + exists (`]-oo, z[%classic, U `&` `]z, +oo[) => /=. + split; [|apply: filterI =>//]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy]. + - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy]. + case=> a b /= [] + []; rewrite !in_itv andbT /= => az Ub zb. + by rewrite (max_r (ltW (lt_trans az _))). +exists (`]-oo, y[%classic, U `&` `]x, +oo[) => /=. + split; [|apply: filterI => //]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE]. + - by split; [exact: rray_open|rewrite set_itvE]. +case=> a b /=; rewrite !in_itv /= andbT => [/=] [ay] [Ub] xb. +rewrite max_r// leNgt; apply: contra_notN (xNy b) => ba. +by rewrite xb (lt_trans ba). Qed. -Lemma max_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} +Lemma max_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} (f g : X -> T): continuous f -> continuous g -> continuous (f \max g). Proof. -move=> fc gc z; apply: continuous2_cvg; first apply max_continuous. - exact: fc. -exact: gc. +move=> fc gc z; apply: continuous2_cvg; [|exact: fc|exact: gc]. +by apply max_continuous. Qed.