composition is continuous (#1388)

* composition is continuous

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -93,6 +93,15 @@
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
+- in file `boolp.v`,
+  + new lemmas `uncurryK`, and `curryK`
+- in file `weak_topology.v`,
+  + new lemma `continuous_comp_weak`
+- in file `function_spaces.v`,
+  + new definition `eval`
+  + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`, 
+    `eval_continuous`, and `compose_continuous`
+
 ### Changed
 
 - in file `normedtype.v`,

classical/boolp.v

@@ -969,3 +969,9 @@ Lemma inhabited_witness: inhabited T -> T.
 Proof. by rewrite inhabitedE => /cid[]. Qed.
 
 End Inhabited.
+
+Lemma uncurryK {X Y Z : Type} : cancel (@uncurry X Y Z) curry.
+Proof. by move=> f; rewrite funeq2E. Qed.
+
+Lemma curryK {X Y Z : Type} : cancel curry (@uncurry X Y Z).
+Proof. by move=> f; rewrite funeqE=> -[]. Qed.

theories/function_spaces.v

@@ -70,6 +70,7 @@ From mathcomp Require Import reals signed topology separation_axioms.
 (*   {family fam, F --> f} == F converges to f in {family fam, U -> V}        *)
 (*  {compact_open, U -> V} == compact-open topology                           *)
 (* {compact_open, F --> f} == F converges to f in {compact_open, U -> V}      *)
+(*                    eval == the evaluation map for continuous functions     *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Ascoli's theorem notations                                              *)
@@ -1436,6 +1437,17 @@ move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O).
 by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO.
 Unshelve. all: by end_near. Qed.
 
+Lemma continuous_curry_fun (f : U * V -> W) :
+  continuous f -> continuous (curry f).
+Proof. by case/continuous_curry. Qed.
+
+Lemma continuous_curry_cvg (f : U * V -> W) (u : U) (v : V) :
+  continuous f -> curry f z.1 z.2 @[z --> (u, v)] --> curry f u v.
+Proof.
+move=> cf D /cf; rewrite !nbhs_simpl /curry /=; apply: filterS => z ? /=.
+by rewrite -surjective_pairing.
+Qed.
+
 Lemma continuous_uncurry_regular (f : U -> V -> W) :
   locally_compact [set: V] -> @regular_space V -> continuous f ->
   (forall u, continuous (f u)) -> continuous (uncurry f).
@@ -1544,3 +1556,46 @@ Unshelve. all: by end_near. Qed.
 End cartesian_closed.
 
 End currying.
+
+Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y :=
+  uncurry (id : continuousType X Y -> (X -> Y)).
+
+Section composition.
+
+Local Import ArrowAsCompactOpen.
+
+Lemma eval_continuous {X Y : topologicalType} :
+  locally_compact [set: X] -> regular_space X -> continuous (@eval X Y).
+Proof.
+move=> lcX rsX; apply: continuous_uncurry_regular => //.
+  exact: weak_continuous.
+by move=> ?; exact: cts_fun.
+Qed.
+
+Lemma compose_continuous {X Y Z : topologicalType} :
+  locally_compact [set: X] -> @regular_space X ->
+  locally_compact [set: Y] -> @regular_space Y ->
+  continuous (uncurry
+    (comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)).
+Proof.
+move=> lX rX lY rY; apply: continuous_comp_weak.
+set F := _ \o _.
+rewrite -[F]uncurryK; apply: continuous_curry_fun.
+pose g := uncurry F \o prodAr \o swap; rewrite /= in g *.
+have -> : uncurry F = uncurry F \o prodAr \o prodA by rewrite funeqE => -[[]].
+move=> z; apply: continuous_comp; first exact: prodA_continuous.
+have -> : uncurry F \o prodAr = uncurry F \o prodAr \o swap \o swap.
+  by rewrite funeqE => -[[]].
+apply: continuous_comp; first exact: swap_continuous.
+pose h (fxg : continuousType X Y * X * continuousType Y Z) : Z :=
+  eval (fxg.2, (eval fxg.1)).
+have <- : h = uncurry F \o prodAr \o swap.
+  by rewrite /h/g/uncurry/swap/F funeqE => -[[]].
+rewrite /h.
+apply: (@continuous2_cvg _ _ _ _ _ _ snd (eval \o fst) (curry eval)).
+- by apply: continuous_curry_cvg; exact: eval_continuous.
+- exact: cvg_snd.
+- by apply: cvg_comp; [exact: cvg_fst | exact: eval_continuous].
+Qed.
+
+End composition.

theories/topology_theory/weak_topology.v

@@ -211,3 +211,11 @@ move=> [][][[]l|[]] [[]r|[]][][]//= _ xlr /filterS; apply.
 Qed.
 
 End weak_order_refine.
+
+Lemma continuous_comp_weak {Y : choiceType} {X Z : topologicalType} (w : Y -> Z)
+  (f : X -> weak_topology w) :
+  continuous (w \o f) -> continuous f.
+Proof.
+move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf.
+exact: open_nbhs_nbhs.
+Qed.