proposition: Lemma comp_resp_uni_continuous : uni_continuous f -> uni_continuous g -> uni_continuous (compose_CSetoid_fun X B C f g).
proof: Proof. unfold uni_continuous in |- *. intros H H0. simpl in |- *. intros n H1. elim H0 with n H1. intro x. intro H3. elim H with x H1. intro x0. intro H4. exists x0. intros x1 y H5. apply H3. apply H4. exact H5. Qed.
imports: CoRN.metrics.CPseudoMSpaces