proposition: Lemma const_fun_is_uni_continuous : forall b : B, uni_continuous (Const_CSetoid_fun X B b).
proof: Proof. intro b. apply lipschitz_imp_uni_continuous. apply const_fun_is_lipschitz. Qed.
imports: CoRN.metrics.CPseudoMSpaces