proposition: Lemma f_uni_cont: uni_continuous f.
proof: Proof. assert (lipschitz' f). apply (lip_c_imp_lip (SubMetricSpace M P) IR_as_CMetricSpace f C). apply f_lip. assert (lipschitz f). apply (lipschitz'_imp_lipschitz (SubMetricSpace M P) IR_as_CMetricSpace f); auto. apply lipschitz_imp_uni_continuous; auto. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory