proposition: Lemma lip_extension_keeps_fun : forall (x : SubMetricSpace M P), lip_extension (from_SubPsMetricSpace M P x) [=] f x.
proof: Proof. intros. unfold lip_extension. simpl. unfold lip_extension_f. elim inf_f_multi_ext_exists. unfold set_glb_IR. simpl. intros y H. destruct H as [l s]. apply leEq_imp_eq. apply l. exists x. assert (dsub' M P (from_SubPsMetricSpace M P x) x[=][0]). unfold dsub'. assert (diag_zero M (cms_d (c:=M))). apply pos_imp_ap_imp_diag_zero. apply ax_d_pos_imp_ap. apply (CPsMetricSpace_is_CPsMetricSpace M). apply ax_d_nneg. apply (CPsMetricSpace_is_CPsMetricSpace M). apply H. astepl (f x[+]C[*][0]). astepl (f x[+][0]). algebra. assert (forall e : IR, [0] [<]e -> f x [-] y [<] e). intros. assert (sig2T IR (fun x0 : IR => sigT (fun x1 : subcsetoid_crr M P => f x1[+]C[*]dsub' M P (from_SubPsMetricSpace M P x) x1[=]x0)) (fun x : IR => x[-]y[<]e)). apply s. auto. destruct X0. destruct s0. assert (f x [<=] f x1[+]C[*]dsub' M P (from_SubPsMetricSpace M P x) x1). astepr (C[*] dsub' M P (from_SubPsMetricSpace M P x) x1 [+] f x1). apply shift_leEq_plus. apply lip_unfolded. apply leEq_less_trans with (f x1[+]C[*]dsub' M P (from_SubPsMetricSpace M P x) x1[-]y). apply minus_resp_leEq; auto. astepl (x0 [-] y); auto. astepl (f x [-] y [+] y). astepr ([0] [+] y). apply plus_resp_leEq. apply approach_zero; auto. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory