proposition: Lemma graphPoint_uc : is_UniformlyContinuousFunction (graphPoint_raw f) graphPoint_modulus.
proof: Proof. intros e a b H. unfold graphPoint_modulus in *. split. change (ball_ex e a b). eapply ball_ex_weak_le;[|apply H]. destruct (mu f e) as [d|]. apply Qpos_min_lb_l. apply Qle_refl. apply uc_prf. eapply ball_ex_weak_le;[|apply H]. destruct (mu f e) as [d|]. apply Qpos_min_lb_r. constructor. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.metric2.Compact CoRN.metric2.Prelength CoRN.metric2.CompleteProduct CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.logic.Classic