proposition: Lemma Cap_fun_prf X Y plX (f:Complete (X --> Y)) (x:Complete X) : is_RegularFunction (@ball Y) (Cap_raw plX f x).
proof: Proof. intros e1 e2. pose (exist (Qlt 0) (1#2) eq_refl) as half. unfold Cap_raw. unfold Cap_raw. unfold QposInf_mult, QposInf_bind. set (he1 := (half * e1)%Qpos). set (he2 := (half * e2)%Qpos). set (f1 := (approximate f he1)). set (f2 := (approximate f he2)). change (Cmap (Y:=Y) plX f1) with (Cmap_strong Y plX f1). change (Cmap (Y:=Y) plX f2) with (Cmap_strong Y plX f2). set (y1 :=(Cmap_strong Y plX f1 x)). set (y2 :=(Cmap_strong Y plX f2 x)). setoid_replace (proj1_sig e1 + proj1_sig e2) with (proj1_sig (he1 + (he1 + he2) + he2))%Qpos by (simpl; ring). rewrite <- ball_Cunit. apply ball_triangle with y2;[|apply ball_approx_r]. apply ball_triangle with y1;[apply ball_approx_l|]. apply (uc_prf (Cmap_strong Y plX)). apply (@regFun_prf _ (@ball (X-->Y))). 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