proposition: Lemma lip_unfolded : forall (x x1: SubMetricSpace M P), f x[-]f x1[<=]C[*]dsub' M P (from_SubPsMetricSpace M P x) x1.
proof: Proof. intros. unfold dsub'. astepr (C[*](x[-d]x1)). apply leEq_transitive with (AbsIR (f x[-] f x1)). apply leEq_AbsIR. astepl (f x[-d]f x1). assert (lipschitz_c f C). apply f_lip. apply X. apply mult_wd; algebra. case x. case x1. intros. simpl. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory