Example of a Complete Metric Space: BoundedFunction

Definition BoundedFunction := Complete LinfStepQ.

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