proposition: Lemma curry_continuous (f : (U * V)%type ~> W) : continuous f -> @regular_space U -> {for f, continuous (curry : ((U * V)%type ~> W) -> (U ~> V ~> W))}.
proof: Proof. move=> ctsf regU; apply/compact_open_cvgP. by apply: fmap_filter; exact: nbhs_filter. move=> K ? cptK [D OfinIo <-] fKD /=; near=> z => w [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP : (cptK); apply => u Ku. have [] := fKD (curry f u); first by exists u. move=> E /[dup] /[swap] /OfinIo [N Asub <- DIN INf]. suff : \forall x' \near u & i \near nbhs f, K x' -> (\bigcap_(i in [set` N]) i) (curry i x'). apply: filter_app; near=> a b => /[apply] ?. by exists (\bigcap_(i in [set` N]) i). apply: filter_bigI_within => R RN; have /set_mem [[M cptM _]] := Asub _ RN. have Rfu : R (curry f u) by exact: INf. move/(_ _ Rfu) => [O [fMO oO] MOR]; near=> p => /= Ki; apply: MOR => + [+ + <-]. move=> _ v Mv; move: v Mv Ki; near: p. have umb : \forall y \near u, (forall b, M b -> nbhs (y, b) (f @^-1` O)). move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. have [[P Q] [Pu Qv] PQO] : nbhs (u, v) (f @^-1` O). by apply: ctsf; apply: open_nbhs_nbhs; split => //; apply: fMO; exists v. exists (Q, P); [by []| move=> [b a [/= Qb Pa Mb]]]. by apply: ctsf; apply: open_nbhs_nbhs; split => //; exact: PQO. move/compact_near_coveringP/near_covering_withinP : (cptM); apply => v Mv. have [P' P'u cPO] := regU u _ umb. pose L := [set h | h @` ((K `&` closure P') `*` M) `<=` O]. exists (setT, P' `*` L). split => //; [exact: filterT|]; exists (P', L) => //; split => //. apply: open_nbhs_nbhs; split; first apply: compact_open_open => //. apply: compact_setM => //; apply: compact_closedI => //. exact: closed_closure. by move=> ? [[a b] [[Ka /cPO +] Mb <-]] => /(_ _ Mb)/nbhs_singleton. move=> [b [a h]] [/= _ [Pa] +] Ma Ka; apply. by exists (a, b); split => //; split => //; exact/subset_closure. 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