proposition: Lemma is_UniformlyContinuousFunction_wd : forall (f1 f2:X -> Y) (mu1 mu2: Qpos -> QposInf), (forall x, msp_eq (f1 x) (f2 x)) -> (forall x, QposInf_le (mu2 x) (mu1 x)) -> (is_UniformlyContinuousFunction f1 mu1) -> (is_UniformlyContinuousFunction f2 mu2).
proof: Proof. intros f1 f2 mu1 mu2 Hf Hmu H e a b Hab. assert (QposEq e e) by reflexivity. apply (ball_wd Y H0 _ _ (Hf a) _ _ (Hf b)). apply H. eapply ball_ex_weak_le. apply Hmu. assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List