proposition: Lemma CSUCextendAdapt : forall {R : ConstructiveReals} (f : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (a b : CRcarrier R), a <= CSUC_low f fL -> CSUC_high f fL <= b -> CSUC (TotalizeFunc (CRcarrier R) f (CSUC_fullDomain f fL)) a b (CSUC_cont_mod f fL).
proof: Proof. split. split. - apply fL. - apply fL. - intros. destruct fL,CSUC_adapt0,u. simpl. simpl in H,H0. rewrite (c x). reflexivity. destruct H1. left. exact (CRlt_le_trans x a _ c2 H). right. exact (CRle_lt_trans _ b x H0 c2). Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets