CoRN.model.metric2.BoundedFunction

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

Set Implicit Arguments.

Open Local Scope uc_scope.

Example of a Complete Metric Space: BoundedFunction

Definition BoundedFunction := Complete LinfStepQ.

Definition sup : BoundedFunction --> CR :=
Cmap LinfStepQPrelengthSpace StepQSup_uc.