fact: Definition CFseq_cvu fn f (x : C) (r : posreal) := forall eps : R, 0 < eps -> exists N : nat, forall n (y : C), (N <= n)%nat -> Boule x r y -> C_dist (fn n y) (f y) < eps.
imports: Cbase Cfunctions Csequence Canalysis_def