fact: Definition uc_compose (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) : X --> Z := Build_UniformlyContinuousFunction (uc_compose_prf g f).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List