proposition: Lemma UniformlyContinuous_proper `{MetricSpaceClass X} `{MetricSpaceClass Y} (f g: X → Y) `{!UniformlyContinuous_mu f} `{!UniformlyContinuous_mu g}: (∀ x, mspc_equiv Y (f x) (g x)) → (∀ e, uc_mu f e ≡ uc_mu g e) → UniformlyContinuous f → UniformlyContinuous g.
proof: Proof. constructor; try apply _. intros ????. pose proof (mspc_ball_proper Y) as H7. rewrite <- (mspc_ball_wd Y e e (f a) (g a) (f b) (g b)). apply (uniformlyContinuous f). rewrite H4. auto. reflexivity. apply H3. apply H3. Qed.
imports: CoRN.algebra.RSetoid Arith List CoRN.model.totalorder.QposMinMax CSetoids Qmetric Qring Qinf QnnInf QnonNeg ProductMetric QposInf Qposclasses UniformContinuity MathClasses.implementations.stdlib_rationals stdlib_omissions.Pair stdlib_omissions.Q PointFree MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.theory.products util.Container