fact: Definition IntegrableOpContract {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (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 (X (ElemFunc IS)) f op opEq)) (contract : forall x y : CRcarrier (RealT (ElemFunc IS)), CRabs _ (op x - op y) <= CRabs _ (x - y)) (zeroFix : op 0 == 0) : IntegrableFunction f -> IntegrableFunction (Xop (X (ElemFunc IS)) f op opEq).
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase