proposition: Lemma lipschitz_imp_uni_continuous : forall (C D : CPsMetricSpace) (f : CSetoid_fun C D), lipschitz f -> uni_continuous f.
proof: Proof. red in |- *. unfold lipschitz in |- *. intros C D f H n H0. elim H. intros. exists (n + x). intros x0 y H1. apply leEq_less_trans with (Two[^]x[*](x0[-d]y)). apply p. apply mult_cancel_less with (([1][/] Two:IR[//]H0)[^]x). apply nexp_resp_pos. apply div_resp_pos. apply pos_two. apply pos_one. apply less_wdr with (([1][/] Two:IR[//]H0)[^](n + x)). apply less_wdl with (x0[-d]y). exact H1. astepr (Two[^]x[*](x0[-d]y)[*]([1][^]x[/] Two[^]x[//]nexp_resp_ap_zero x H0)). astepr (Two[^]x[*](x0[-d]y)[*]([1][/] Two[^]x[//]nexp_resp_ap_zero x H0)). rational. apply eq_symmetric_unfolded. astepr (([1][/] Two:IR[//]H0)[^](n + x)). apply nexp_plus. Qed.
imports: CoRN.metrics.CPseudoMSpaces