proposition: Lemma f_multi_ext_uni_continuous : forall y : M, uni_continuous (A:=SubMetricSpace M P) (B:=IR_as_CPsMetricSpace) (f_multi_ext y).
proof: Proof. intros. unfold f_multi_ext. apply (plus_resp_uni_continuous (SubMetricSpace M P) f (cdsub' y) f_uni_cont (cdsub'_uni_cont y)). Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory