proposition: Lemma filterlim_locally_close : forall {F} {FF: ProperFilter F} (f : T -> U) l l', filterlim f F (locally l) -> filterlim f F (locally l') -> close l l'.
proof: Proof. intros F FF f l l' Hl Hl' eps. assert (locally l (ball l (pos_div_2 eps))). by apply locally_ball. specialize (Hl (ball l (pos_div_2 eps)) H). assert (locally l' (ball l' (pos_div_2 eps))). by apply locally_ball. specialize (Hl' (ball l' (pos_div_2 eps)) H0). unfold filtermap in Hl, Hl'. generalize (filter_and _ _ Hl Hl') => {H0} H. apply filter_ex in H. case: H => x H. rewrite (double_var eps). apply ball_triangle with (f x). by apply H. by apply ball_sym, H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub