min and max are continuous (#1387)

* min and max are continuous --------- Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Nov 10, 2024 · 7e2988d · 7e2988d
1 parent f5097d5
commit 7e2988d
Show file tree

Hide file tree

Showing 2 changed files with 80 additions and 1 deletion.
diff --git 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
 

diff --git 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,79 @@ 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; 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) :
+  continuous f -> continuous g -> continuous (f \min g).
+Proof.
+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; 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}
+    (f g : X -> T):
+  continuous f -> continuous g -> continuous (f \max g).
+Proof.
+move=> fc gc z; apply: continuous2_cvg; [|exact: fc|exact: gc].
+by apply max_continuous.
+Qed.