proposition: Lemma unicon_resp_totallybounded : forall (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (H : uni_continuous'' f), MStotally_bounded X -> MStotally_bounded (SubPsMetricSpace (fun y : Z => {x : X | f x[=]y})).
proof: Proof. intros X Z f. unfold uni_continuous'' in |- *. intro H. unfold MStotally_bounded in |- *. intro H1. intro n. elim H. intros mod_ H3. elim (H1 (mod_ n)). intros l H2. simpl in |- *. exists (map (re_co_do X Z f) l). intros x. elim x. intros r H5. elim H5. intros k H6. elim (H2 k). intros m H7 H8. exists (re_co_do X Z f m). 2: simpl in |- *. 2: astepl (f k[-d]f m). 2: apply H3. 2: exact H8. apply map_member'. exact H7. Qed.
imports: CoRN.metrics.Prod_Sub