fact: Definition MSseqLimit (X : CPsMetricSpace) (seq : nat -> X) (lim : X) : CProp := forall (n : nat) (H : Two[#][0]), {N : nat | forall m : nat, N <= m -> seq m[-d]lim[<]([1][/] Two:IR[//]H)[^]n}.
imports: CoRN.metrics.CPseudoMSpaces