proposition: Lemma prod_to_single {T U V : UniformSpace} {F: (U -> Prop) -> Prop} {FF : Filter F} (G : (V -> Prop) -> Prop) x (f : T -> U -> V) : filterlim (fun tu : T * U => f tu.1 tu.2) (filter_prod (at_point x) F) G <-> filterlim (fun u : U => f x u) F G.
proof: Proof. split => H P GP. - rewrite /filtermap. destruct (H _ GP) as [Q R HAQ HFR HPf]. apply: filter_imp HFR => y HRy. exact: HPf. - specialize (H P GP). econstructor. exact: Logic.eq_refl. exact: H. by move => t u <-. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp