proposition: Lemma const_fun_is_continuous : forall b : B, continuous (Const_CSetoid_fun X B b).
proof: Proof. intro b. apply uni_continuous_imp_continuous. apply const_fun_is_uni_continuous. Qed.
imports: CoRN.metrics.CPseudoMSpaces