proposition: Lemma filterlim_closely {T} {U : UniformSpace} {F : (T -> Prop) -> Prop} {FF : Filter F} (f : T -> U) : filterlim (fun x => (f (fst x), f (snd x))) (filter_prod F F) closely <-> (forall eps : posreal, exists P, F P /\ forall u v : T, P u -> P v -> ball (f u) eps (f v)).
proof: Proof. apply filterlim_prod. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub