proposition: Lemma extension_also_liscphitz : lipschitz_c (lip_extension) C.
proof: Proof. unfold lipschitz_c. unfold lip_extension. unfold lip_extension_f. intros y1 y2. intros. simpl. elim inf_f_multi_ext_exists. elim inf_f_multi_ext_exists. unfold f_multi_ext. unfold dIR. simpl. intros fy2 Hfy2 fy1 Hfy1. apply AbsSmall_imp_AbsIR. assert (forall e : IR, [0][<]e -> AbsSmall (C[*](y1[-d]y2)[+]e) (fy1[-]fy2)). intros. unfold AbsSmall. split. astepr ([--](fy2 [-] fy1)). apply inv_resp_leEq. apply extension_also_lipschitz_case; auto. rational. astepr (C[*](y2[-d]y1)[+]e). astepl (fy1 [-] fy2). apply (extension_also_lipschitz_case y2 y1 fy1 Hfy1 fy2 Hfy2 e X). assert (y2[-d]y1[=]y1[-d]y2). apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. algebra. apply AbsSmall_approach. auto. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory