proposition: Lemma telescopicOpL : forall {IS : IntegrationSpace} (fn : nat -> PartialFunction (X (ElemFunc IS))) (fnL : forall n:nat, L (ElemFunc IS) (fn n)) (op : CRcarrier (RealT (ElemFunc IS)) -> CRcarrier (RealT (ElemFunc IS))) (opEq : forall x y : CRcarrier (RealT (ElemFunc IS)), x == y -> op x == op y) (opL : forall f : PartialFunction (X (ElemFunc IS)), L (ElemFunc IS) f -> L (ElemFunc IS) (Xop _ f op opEq)) (n : nat), L (ElemFunc IS) (telescopicOp (X (ElemFunc IS)) fn op opEq n).
proof: Proof. intros. unfold telescopicOp. destruct n. apply opL. apply fnL. unfold Xminus. apply LplusStable. apply opL. apply LsumStable. apply fnL. apply LscaleStable. apply opL. apply LsumStable. apply fnL. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase