composition is continuous

CHANGELOG_UNRELEASED.md

@@ -92,6 +92,15 @@
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
+- in file `functions.v`,
+  + new lemmas `uncurryK`, and `curryK`.
+- in file `weak_topology.v`,
+  + new lemma `continuous_comp_weak`.
+- in file `function_spaces.v`,
+  + new definitions `eval`, and `comp_cts`.
+  + new lemmas `continuous_curry_fun`, `continuous_curry_joint_cvg`, 
+    `eval_continuous`, and `compose_continuous`.
+
 ### Changed
 
 - in file `normedtype.v`,

classical/functions.v

@@ -2665,3 +2665,9 @@ End function_space_lemmas.
 
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : f\^-1\^-1%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
+
+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; case=> ? ?. Qed.

theories/function_spaces.v

@@ -70,6 +70,8 @@ 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     *)
+(*                comp_cts == composition for continuous functions            *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Ascoli's theorem notations                                              *)
@@ -1436,6 +1438,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_joint_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 move=> ?; 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 +1557,51 @@ 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)).
+
+Definition comp_cts {X Y Z : topologicalType} (g : continuousType Y Z)
+    (f : continuousType X Y) : continuousType X Z :=
+  g \o f.
+
+Section composition.
+
+Local Import ArrowAsCompactOpen.
+
+Lemma eval_continuous {X Y : topologicalType} : 
+  locally_compact [set: X] -> regular_space X -> continuous (@eval X Y).
+Proof.
+move=> ? ?; 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_cts X Y Z)).
+Proof.
+move=> ? ? lY rY; apply: continuous_comp_weak.
+set F := _ \o _.
+rewrite -[F]uncurryK; apply: continuous_curry_fun.
+pose g := uncurry F \o prodAr \o (@swap _ _); simpl in *.
+have -> : uncurry F = uncurry F \o prodAr \o prodA.
+  by rewrite funeqE; case; case.
+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; case; case.
+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; case; case.
+rewrite /h.
+apply: (@continuous2_cvg _ _ _ _ _ _ (snd) (eval \o fst) (curry eval)).
+- by apply: continuous_curry_joint_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.
+by apply: open_nbhs_nbhs; split.
+Qed.