proposition: Lemma uc_compose_prf (X Y Z:MetricSpace) (g: Y --> Z) (f:X --> Y) : is_UniformlyContinuousFunction (fun x => g (f x)) (fun e => QposInf_bind (mu f) (mu g e)).
proof: Proof. revert g f. intros [g mu_g Hg] [f mu_f Hf] e a b Hab. unfold is_UniformlyContinuousFunction in *. simpl in *. apply Hg. clear Hg. destruct (mu_g e) as [mge|]; firstorder. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List