proposition: Lemma filterlimi_locally_close : forall {F} {FF: ProperFilter F} (f : T -> U -> Prop) l l', F (fun x => forall y1 y2, f x y1 -> f x y2 -> y1 = y2) -> filterlimi f F (locally l) -> filterlimi f F (locally l') -> close l l'.
proof: Proof. intros F FF f l l' Hf Hl Hl' eps. assert (H: locally l (ball l (pos_div_2 eps))). by apply locally_ball. specialize (Hl (ball l (pos_div_2 eps)) H). assert (H': locally l' (ball l' (pos_div_2 eps))). by apply locally_ball. specialize (Hl' (ball l' (pos_div_2 eps)) H'). unfold filtermapi in Hl, Hl'. generalize (filter_and _ _ Hf (filter_and _ _ Hl Hl')) => {H' Hl Hl' Hf} H. apply filter_ex in H. destruct H as [x [Hf [[y [H1 H1']] [y' [H2 H2']]]]]. rewrite (double_var eps). apply ball_triangle with y. exact H1'. apply ball_sym. rewrite (Hf _ _ H1 H2). exact H2'. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub