proposition: Lemma filterlimi_const_loc {T} {U : UniformSpace} {F : (T -> Prop) -> Prop} {FF : Filter F} : forall (f : T -> U -> Prop) (a : U), F (fun x => f x a) -> filterlimi f F (locally a).
proof: Proof. intros f a Hf P HP. rewrite /filtermapi /=. apply: filter_imp Hf => x H. exists a. apply (conj H). exact: locally_singleton. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl