proposition: Lemma supremum_exists : forall (X : CPsMetricSpace) (f : CSetoid_fun X IR_as_CPsMetricSpace), uni_continuous'' f -> MStotally_bounded X -> forall x : X, {z : IR | set_lub_IR (fun y : IR_as_CPsMetricSpace => {x : X | f x[=]y}) z}.
proof: Proof. intros X f H0 H1 x. apply totally_bounded_has_lub. apply MStotallybounded_totallybounded. 3: apply unicon_resp_totallybounded. 3: exact H0. 3: exact H1. 2: unfold IR_as_CPsMetricSpace in |- *. 2: simpl in |- *. 2: apply re_co_do_well_def. exists (f x). exists x. apply eq_reflexive. Qed.
imports: CoRN.metrics.Prod_Sub