proposition: Lemma Cap_weak_prf X Y plX (f:Complete (X --> Y)) : is_UniformlyContinuousFunction (Cap_fun plX f) (Cap_modulus f).
proof: Proof. intros e x y H. set (e' := ((1#3)*e)%Qpos). setoid_replace (proj1_sig e) with (proj1_sig (e'+e'+e')%Qpos) by (simpl; ring). apply ball_triangle with (Cmap plX (approximate f e') y). apply ball_triangle with (Cmap plX (approximate f e') x). - apply (ball_wd _ eq_refl _ _ (Cap_fun_correct plX f x) _ _ (reflexivity _)). simpl (Cmap plX (approximate f e') x). apply (ball_wd _ eq_refl _ _ (reflexivity _) _ _ (Cmap_fun_correct _ _ _)). apply Cap_slow_help. - apply (uc_prf). apply H. - apply ball_sym. apply (ball_wd _ eq_refl _ _ (Cap_fun_correct plX f y) _ _ (reflexivity _)). simpl (Cmap plX (approximate f e') y). apply (ball_wd _ eq_refl _ _ (reflexivity _) _ _ (Cmap_fun_correct _ _ _)). apply Cap_slow_help. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q