fact: Definition CVS_dom (fn : nat -> R -> R) (D : R -> Prop) := forall x : R, D x -> ex_finite_lim_seq (fun n => fn n x).
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Continuity Derive Series Lub Hierarchy