proposition: Lemma CSUCext : forall {R : ConstructiveReals} (f g : PartialFunction (CRcarrier R)), PartialFunExtEq f g -> Is_CSUC_func f -> Is_CSUC_func g.
proof: Proof. intros R f g H H0. destruct f,g,H,H0,p; simpl in d. simpl in CSUC_fullDomain0. apply (Build_Is_CSUC_func R {| Domain := Domain0; partialApply := partialApply0; DomainProp := DomainProp0 |} (fun x => d x (CSUC_fullDomain0 x)) CSUC_low0 CSUC_high0 CSUC_lowHigh0 CSUC_cont_mod0). split. apply (UC_ext (TotalizeFunc (CRcarrier R) {| Domain := Domain; partialApply := partialApply; DomainProp := DomainProp |} CSUC_fullDomain0)). apply CSUC_adapt0. intro x. simpl. apply c. intros. simpl. destruct CSUC_adapt0. simpl in c, c0. rewrite <- (c x (CSUC_fullDomain0 x)). apply c0. exact H. Defined.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets