proposition: 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 : (U * V)%type ~> W).
proof: Proof. move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE => -[O [oO Ofuv]] /filterS. apply; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB]. have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z). have [] := reg v (f u @^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. by move=> R ? ?; exists R. exists (f @^-1` [set g | g @` (B `&` closure R) `<=` O], B `&` closure R). split; [apply/cf/open_nbhs_nbhs; split | apply: filterI] => //. - apply: compact_open_open => //; apply: compact_closedI => //. exact: closed_closure. - by move=> ? [x [? + <-]]; apply: RO. - by apply: filterS; first exact: subset_closure. by case=> a r /= [fBMO [Br] cmR]; apply: fBMO; exists r. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed