proposition: Lemma Cmap_strong_slow_prf : is_UniformlyContinuousFunction ((Cmap_slow (Y:=Y)):(X_Y -> CX_CY)) Qpos2QposInf.
proof: Proof. intros e f g H. split. apply Qpos_nonneg. intro x. apply ball_closed. intros e0 epos. set (he0 := ((1#2)*exist _ _ epos)%Qpos). set (d0 := QposInf_min (Qpos2QposInf (1#2)*(mu f he0)) (Qpos2QposInf (1#2)*(mu g he0))). set (a0 := approximate x d0). setoid_replace (proj1_sig e+e0) with (proj1_sig (he0 + e + he0)%Qpos) by (simpl; ring). apply ball_triangle with (Cunit (g a0)). apply ball_triangle with (Cunit (f a0)). assert (QposEq he0 he0) by reflexivity. pose proof (MonadLaw3 f a0). symmetry in H1. apply (ball_wd _ H0 _ _ (reflexivity _) _ _ H1). clear H1 H0. refine (uc_prf _ _ _ _ _). simpl. destruct (mu f he0) as [d1|];[|constructor]. eapply ball_ex_weak_le with d0. apply QposInf_min_lb_l. destruct d0 as [d0|];[|constructor]. apply ball_approx_r. rewrite -> ball_Cunit. apply H. assert (QposEq he0 he0) by reflexivity. pose proof (MonadLaw3 g a0). symmetry in H1. apply (ball_wd _ H0 _ _ H1 _ _ (reflexivity _)). clear H1 H0. apply (uc_prf (Cmap_slow g)). simpl. destruct (mu g he0) as [d2|];[|constructor]. eapply ball_ex_weak_le with d0. apply QposInf_min_lb_r. destruct d0 as [d0|];[|constructor]. apply ball_approx_l. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax