proposition: Lemma filterlim_locally : forall {F} {FF : Filter F} (f : T -> U) y, filterlim f F (locally y) <-> forall eps : posreal, F (fun x => ball y eps (f x)).
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]. apply: filter_imp (Cf eps). intros t. apply He. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub