proposition: Lemma inf_f_multi_ext_exists : forall y : M, {z : IR | set_glb_IR (fun v : IR_as_CMetricSpace => {x : SubMetricSpace M P | f_multi_ext y x[=]v}) z}.
proof: Proof. intros. elim (infimum_exists (SubMetricSpace M P) (f_multi_ext y)). 3: apply set_bounded. intros x H. exists x. apply H. assert (uni_continuous (f_multi_ext y)). apply f_multi_ext_uni_continuous. assert (uni_continuous' (f_multi_ext y)). apply uni_continuous_imp_uni_continuous'; auto. apply uni_continuous'_imp_uni_continuous''; auto. elim non_empty. intros x H. exists x. apply H. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory