proposition: Lemma extension_also_lipschitz_case : forall (y1 : M) (y2 : M) (fy2 : IR) (Hfy2 : set_glb_IR (fun v : IR => sigT (fun x : subcsetoid_crr M P => f x[+]C[*]dsub' M P y2 x[=]v)) fy2) (fy1 : IR) (Hfy1 : set_glb_IR (fun v : IR => sigT (fun x : subcsetoid_crr M P => f x[+]C[*]dsub' M P y1 x[=]v)) fy1) (e : IR) (X : [0][<]e), fy2[-]fy1[<=]C[*](y1[-d]y2)[+]e.
proof: Proof. intros. destruct Hfy1. destruct Hfy2 as [l0 s0]. assert ({x : IR | sigT (fun x0 : SubMetricSpace M P => f x0[+]C[*]dsub' M P y1 x0[=]x) | x[-]fy1[<]e}). apply s. auto. destruct X0 as [fx1 Ht Hl1]. destruct Ht as [x1 He1]. assert (fy2 [<=] f x1[+]C[*]dsub' M P y2 x1). apply l0; auto. exists x1. apply eq_reflexive_unfolded. assert (fx1[-]e[<=]fy1). apply less_leEq. apply shift_minus_less. apply shift_less_plus'; auto. apply leEq_transitive with ((f x1[+]C[*]dsub' M P y2 x1)[-](fx1[-]e)). apply minus_resp_leEq_both; auto. astepl (f x1[+]C[*]dsub' M P y2 x1[-]fx1[+]e). apply plus_resp_leEq. astepl (f x1[+]C[*]dsub' M P y2 x1[-](f x1[+]C[*]dsub' M P y1 x1)). astepl (f x1[+]C[*]dsub' M P y2 x1[-]f x1[-]C[*]dsub' M P y1 x1). astepl (f x1[-]f x1[+]C[*]dsub' M P y2 x1[-]C[*]dsub' M P y1 x1). astepl ([0][+]C[*]dsub' M P y2 x1[-]C[*]dsub' M P y1 x1). astepl (C[*]dsub' M P y2 x1[-]C[*]dsub' M P y1 x1). astepl (C[*](dsub' M P y2 x1[-]dsub' M P y1 x1)). apply mult_resp_leEq_lft. 2: apply less_leEq. 2: apply constant_positive. unfold dsub'. astepr (y2[-d]y1). apply leEq_transitive with (AbsIR ((from_SubPsMetricSpace M P x1[-d]y2)[-] (from_SubPsMetricSpace M P x1[-d]y1))). apply leEq_AbsIR. apply AbsSmall_imp_AbsIR. apply rev_tri_ineq. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. rational. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory