proposition: Lemma lift_eq_complete {X Y : MetricSpace} (f g : Complete X --> Y) : (forall x : X, msp_eq (f (Cunit x)) (g (Cunit x))) -> (forall x : Complete X, msp_eq (f x) (g x)).
proof: Proof. intros A x. apply ball_eq; intros e epos. pose (exist (Qlt 0) (1#2) eq_refl) as half. set (e2 := (half * exist _ _ epos)%Qpos). set (d := QposInf_min (mu f e2) (mu g e2)). setoid_replace e with (proj1_sig (e2+e2)%Qpos) by (simpl; ring). apply ball_triangle with (b := f (Cunit (approximate x d))). + apply (UniformContinuity.uc_prf f). apply (ball_ex_weak_le _ d); [apply QposInf_min_lb_l | apply ball_ex_approx_r]. + apply (ball_wd _ eq_refl _ _ (A (approximate x d)) _ _ (reflexivity _)). apply (UniformContinuity.uc_prf g). apply (ball_ex_weak_le _ d); [apply QposInf_min_lb_r | apply ball_ex_approx_l]. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax