proposition: Lemma filterlimi_locally : forall {F} {FF : Filter F} (f : T -> U -> Prop) y, filterlimi f F (locally y) <-> forall eps : posreal, F (fun x => exists z, f x z /\ ball y eps z).
proof: Proof. intros F FF f y. split. - intros Cf eps. apply (Cf (fun x => ball y eps x)). now exists eps. - intros Cf P [eps He]. unfold filtermapi. apply: filter_imp (Cf eps). intros t [z [Hz1 Hz2]]. exists z. apply (conj Hz1). now apply He. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub