proposition: Lemma continuous_uncurry (f : U ~> V ~> W) : locally_compact [set: V] -> hausdorff_space V -> continuous f -> (forall u, continuous (f u)) -> continuous ((uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W)) f).
proof: Proof. move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //. move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. by move=> z; exact: (@compact_regular V hsdf v B). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed