proposition: Lemma uncurry_continuous (f : U ~> V ~> W) : locally_compact [set: V] -> @regular_space V -> @regular_space U -> continuous f -> (forall u, continuous (f u)) -> {for f, continuous (uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W))}.
proof: Proof. move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. by apply: fmap_filter; exact:nbhs_filter. move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. move/compact_near_coveringP/near_covering_withinP: (cptK); apply. case=> u v Kuv. have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. have : continuous (uncurry f) by exact: continuous_uncurry_regular. move/continuousP/(_ _ oO); rewrite openE => /(_ (u, v))[]. by apply: fKO; exists (u, v). case=> /= P' Q' [P'u Q'v] PQO. have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. have [P Pu cPP'] := regU u P' P'u; have [Q Qv cQQ'] := regV v Q' Q'v. exists (closure P), (B `&` closure Q); split. - exact: closed_closure. - by apply: compact_closedI => //; exact: closed_closure. - by apply: filterS; first exact: subset_closure. - by apply: filterI=> //; apply: filterS; first exact: subset_closure. - by case => a b [/cPP' ?] [_ /cQQ' ?]; exact: PQO. case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. (have oR : open R by exact: compact_open_open); pose P' := f @^-1` R. pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. exists ((P `&` P') `*` Q, L); first split => /=. - exists (P `&` P', Q) => //; split => //=; apply: filterI => //. apply: ctsf; apply: open_nbhs_nbhs; split => // _ [b Qb <-]. by apply: (PQfO (u, b)); split => //; exact: nbhs_singleton. - rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. apply: compact_open_open => //; apply: compact_closedI => //. apply: continuous_compact => //; apply: continuous_subspaceT => x. exact: cvg_fst. move=> /= _ [a [Kxa Pa] <-] _ [b Qb <-]. by apply: (PQfO (a, b)); split => //; exact: nbhs_singleton. move=> [[a b h]] [/= [[Pa P'a] Qb Lh] Kab]. apply: (Lh (h a)); first by exists a => //; split => //; exists (a, b). by exists b. 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