proposition: Lemma SigmaFiniteLimit : forall {R : ConstructiveReals} (A : CRcarrier R -> Prop), @PartialRestriction R _ (XpointwiseLimit (fun n => CharacFunc (fun x => -CR_of_Q R (Z.of_nat n # 1) <= x /\ x <= CR_of_Q R (Z.of_nat n # 1) /\ A x))) (CharacFunc A).
proof: Proof. split. - intros x [xnD H]. destruct (CRup_nat (CRabs _ x)) as [n H0]. apply CRabs_lt in H0. destruct H0. destruct (xnD n) as [isin|isout]. + left. apply isin. + right. intro abs. apply isout. repeat split. 3: exact abs. 2: apply CRlt_asym, c. rewrite <- (CRopp_involutive x). apply CRopp_ge_le_contravar. apply CRlt_asym, c0. - intros. simpl. destruct (CRup_nat (CRabs _ x)) as [n nup]. apply CRabs_lt in nup. destruct nup. destruct xD as [xnD H], xG. + unfold CharacFunc, Domain, inject_Z in xnD. unfold CharacFunc, partialApply in H. apply Rcauchy_complete_cv. intro p. exists n. intros. destruct (xnD i). unfold CRminus. rewrite CRplus_opp_r. rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. exfalso. apply n0. repeat split. 3: exact a. rewrite <- (CRopp_involutive x). apply CRopp_ge_le_contravar. apply (CRle_trans _ (CR_of_Q R (Z.of_nat n # 1))). apply CRlt_asym, c0. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, H0. apply (CRle_trans _ (CR_of_Q R (Z.of_nat n # 1))). apply CRlt_asym, c. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, H0. + unfold CharacFunc, partialApply in H. apply Rcauchy_complete_cv. intro p. exists O. intros. destruct (xnD i). exfalso. destruct a, H2. contradiction. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile