proposition: Lemma IntegrableApproxSequenceInc : forall {IS : IntegrationSpace} (gen : IntegrableSetsGen IS) (A : X (ElemFunc IS) -> Prop) (Aint : IntegrableSet A) (n : nat) (x : X (ElemFunc IS)), let (U,_) := IntegrableApproxSequence gen A Aint n in U x -> A x.
proof: Proof. induction n. - intros. simpl. destruct (gen A Aint 1 (CRzero_lt_one (RealT (ElemFunc IS)))). apply sa_inc0. - intros. simpl. destruct (IntegrableApproxSequence gen A Aint n). intros. destruct H. apply IHn, H. apply (sa_inc _ _ _ _ x H). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile