proposition: Lemma comp_resp_continuous : continuous f -> continuous g -> continuous (compose_CSetoid_fun X B C f g).
proof: Proof. unfold continuous in |- *. intros H H0 x n H1. simpl in |- *. elim H0 with (f x) n H1. intros. elim H with x x0 H1. intros. exists x1. intros y H2. apply p. apply p0. exact H2. Qed.
imports: CoRN.metrics.CPseudoMSpaces