CoRN.model.metric2.IntegrableFunction


Require Export Complete.
Require Import CRmetric.
Require Import L1metric.
Require Import LinfMetric.
Require Import Qmetric.
Require Import CornTac.
Require Import BoundedFunction.

Set Implicit Arguments.

Open Local Scope uc_scope.

Example of a Complete Metric Space: IntegrableFunction

Definition IntegrableFunction := Complete L1StepQ.

Definition Integral : IntegrableFunction --> CR :=
 Cmap L1StepQPrelengthSpace IntegralQ_uc.

Every bounded function is integrable.
Definition BoundedAsIntegrable : BoundedFunction --> IntegrableFunction :=
 Cmap LinfStepQPrelengthSpace LinfAsL1.