proposition: Lemma graphPoint_b_uc : is_UniformlyContinuousFunction (graphPoint_b_raw f) (graphPoint_modulus f).
proof: Proof. intros e a b H d1 d2. split. change (ball_ex (Qpos2QposInf d1 + e + Qpos2QposInf d2) a b). eapply ball_ex_weak_le;[|apply H]. unfold graphPoint_modulus. destruct (mu f e) as [d|]. - simpl. apply Qle_trans with (proj1_sig e + 0). rewrite Qplus_0_r. apply Qpos_min_lb_l. rewrite <- (Qplus_comm (proj1_sig e)), <- Qplus_assoc. apply Qplus_le_r. apply (Qpos_nonneg (d1+d2)). - simpl. apply Qle_trans with (proj1_sig e + 0). rewrite Qplus_0_r. apply Qle_refl. rewrite <- (Qplus_comm (proj1_sig e)), <- Qplus_assoc. apply Qplus_le_r. apply (Qpos_nonneg (d1+d2)). - simpl. revert d1 d2. change (ball (proj1_sig e) (f a) (f b)). apply uc_prf. eapply ball_ex_weak_le;[|apply H]. unfold graphPoint_modulus. 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