proposition: Lemma cauchy_distance' : forall {T : UniformSpace} {F} {FF : ProperFilter F}, cauchy F <-> filter_le (filter_prod F F) (@closely T).
proof: Proof. intros T F FF. split. - intros H P [eps HP]. case: (H (pos_div_2 eps)) => {H} x Hx. split with (1 := Hx) (2 := Hx). move => u v Hu Hv. apply HP. rewrite (double_var eps). apply ball_triangle with x. by apply ball_sym. exact Hv. - intros H eps. destruct (H (fun '(u,v) => ball u eps v)) as [P Q HP HQ H']. now exists eps. destruct (filter_ex P HP) as [x Hx]. exists x. move: (fun v => H' x v Hx) => {H'} H. now apply filter_imp with (1 := H). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub