proposition: Lemma applyDiagAbs : forall {R : ConstructiveReals} {X : Set} (fnk : nat -> nat -> PartialFunction X) (x : X) (cpxDdiag : forall k : nat, Domain (diagSeq (fun n k0 : nat => Xabs (fnk n k0)) k) x) (cpxDdiagBis : forall k : nat, Domain (diagSeq fnk k) x) (k : nat), partialApply _ x (cpxDdiag k) == CRabs R (partialApply _ x (cpxDdiagBis k)).
proof: Proof. intros. unfold diagSeq. generalize (cpxDdiag k). intro d. generalize (cpxDdiagBis k). intro d0. clear cpxDdiagBis cpxDdiag. unfold diagSeq in d, d0. destruct (diagPlaneInv k). apply CRabs_morph. apply DomainProp. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions