proposition: Lemma binary_uc_prf : is_UniformlyContinuousFunction (g'' : X → (X --> X)) (mu h).
proof: Proof. intros ε x y E. split. apply Qpos_nonneg. intro z. apply Eball_spec. simpl. apply (ball_wd _ (QposEq_refl ε) _ _ (g_eq_h _ _) _ _ (g_eq_h _ _)). apply (uc_prf h). 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