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