proposition: Lemma IntegrableExtensionalAE : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))), almost_everywhere (Domain g) -> almost_everywhere (fun x : X (ElemFunc IS) => forall (dF : Domain f x) (dG : Domain g x), partialApply _ _ dF == partialApply _ _ dG) -> IntegrableFunction f -> IntegrableFunction g.
proof: Proof. intros. destruct X as [h [i c]]. destruct X0 as [k [H H0]]. apply (IntegrableFunctionExtensional (Xplus f (Xplus (Xscale 0 h) (Xscale 0 k)))). - split. + intros x xD. apply c. apply xD. + intros. simpl. destruct xD, d0. rewrite CRmult_0_l, CRmult_0_l, CRplus_0_l, CRplus_0_r. exact (H0 x d1 d xG). - apply (IntegrablePlus _ _ X1). apply IntegrablePlus. apply IntegrableScale, i. apply IntegrableScale, H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions