proposition: Lemma IntegrablePlusMaj : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (g : PartialFunction (X (ElemFunc IS))) (gInt : IntegrableFunction g), PartialRestriction (XinfiniteSumAbs (IntFn (IntegralRepresentationPlus f fInt g gInt))) (Xplus f g).
proof: Proof. split. - intros x xd. exact (IntegralRepresentationPlusInj f fInt g gInt x xd). - intros. apply applyInfiniteSumAbs. destruct fInt as [[fn fnL] [fInj resF]]; destruct gInt as [[gn gnL] [gInj resG]]; unfold IntegralRepresentationPlus, IntFn. unfold IntegralRepresentationPlus, IntFn in xD. pose proof (domainInfinSumWeaveL _ fn gn x xD) as ixf. pose proof (domainInfinSumWeaveR _ fn gn x xD) as ixg. specialize (resF x ixf) as appF. specialize (resG x ixg) as appG. simpl in appG, appF. destruct xG. rewrite (applyXplus f g). rewrite <- appG. rewrite <- appF. apply partialApplyWeaveInfiniteSum. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase