fact: Definition is_UniformlyContinuousFunction (f: X -> Y) (mu: Qpos -> QposInf) := forall e a b, ball_ex (mu e) a b -> ball (proj1_sig e) (f a) (f b).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List