proposition: Lemma continuous_curry (f : (U * V)%type ~> W) : continuous f -> continuous (curry f : U ~> V ~> W) /\ forall u, continuous (curry f u).
proof: Proof. move=> ctsf; split; first last. move=> u z; apply: continuous_comp; last exact: ctsf. by apply: cvg_pair => //=; exact: cvg_cst. move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. near=> z => w /= [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP : cptK; apply. move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed