proposition: Lemma filter_prod_at_point : forall {T F} { FF : Filter F} a (P : R -> T -> Prop) Q, F Q -> (forall y, Q y -> P a y) -> filter_prod (at_point a) F (fun ab : R * T => P ab.1 ab.2).
proof: Proof. intros T F FF a P Q FQ HQ. apply: (Filter_prod _ _ _ (fun x => x = a) Q) => // . - move => x y -> /= H. exact: HQ. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl