fact: Record CommonPointFunSeq {R : ConstructiveReals} (X : Set) (f : @PartialFunction R X) (fn : nat -> @PartialFunction R X) : Set := { cpx : X; cpxF : Domain f cpx; cpxFn : forall n:nat, Domain (fn n) cpx; }.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete