proposition: Lemma IntegrableApproxSequenceIncr : forall {IS : IntegrationSpace} (gen : IntegrableSetsGen IS) (A : X (ElemFunc IS) -> Prop) (Aint : IntegrableSet A) (i j : nat) (x : X (ElemFunc IS)), le i j -> (let (U,_) := IntegrableApproxSequence gen A Aint i in U x) -> (let (U,_) := IntegrableApproxSequence gen A Aint j in U x).
proof: Proof. induction j. - intros. inversion H. subst i. exact H0. - intros. apply Nat.le_succ_r in H. destruct H. specialize (IHj x H). simpl; destruct (IntegrableApproxSequence gen A Aint j). left. exact (IHj H0). subst i. exact H0. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile