proposition: Lemma filterlim_locally_cauchy : forall {F} {FF : ProperFilter F} (f : T -> U), (forall eps : posreal, exists P, F P /\ forall u v : T, P u -> P v -> ball (f u) eps (f v)) <-> exists y, filterlim f F (locally y).
proof: Proof. intros F FF f. apply iff_trans with (2 := filterlim_locally_closely f). apply iff_sym, filterlim_closely. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub