proposition: Lemma CSUC_transport_apply : forall {R : ConstructiveReals} (f g : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f) (pEq : PartialFunExtEq f g) (x : CRcarrier R), TotalizeFunc (CRcarrier R) f (CSUC_fullDomain _ fL) x == TotalizeFunc (CRcarrier R) g (CSUC_fullDomain _ (CSUCext f g pEq fL)) x.
proof: Proof. intros. destruct pEq, p. apply c. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets