proposition: Lemma unary_uc_prf : is_UniformlyContinuousFunction (g' : X → X) (mu h).
proof: Proof. intros ε a b H0. apply Eball_spec. apply (ball_wd _ (QposEq_refl ε) _ _ (g_eq_h _) _ _ (g_eq_h _)). eapply uc_prf. now destruct (mu h ε). Qed.
imports: CoRN.metric2.Metric CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid CoRN.stdlib_omissions.Q CoRN.model.totalorder.QMinMax CoRN.metric2.Complete CoRN.metric2.Prelength MathClasses.interfaces.abstract_algebra