proposition: Lemma together_uc : forall A B C D (f:A --> C) (g:B --> D), is_UniformlyContinuousFunction (fun (p:ProductMS A B) => (f (fst p), g (snd p)):ProductMS C D) (fun x => QposInf_min (mu f x) (mu g x)).
proof: Proof. intros A B C D f g e a b H. split; simpl; apply uc_prf; apply ball_ex_weak_le with (QposInf_min (mu f e) (mu g e)). apply QposInf_min_lb_l. destruct (QposInf_min (mu f e) (mu g e)) as [q|]; auto. destruct H; auto. apply QposInf_min_lb_r. destruct (QposInf_min (mu f e) (mu g e)) as [q|]; auto. destruct H; auto. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.metric2.Classification CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.metric2.Complete CoRN.metric2.LocatedSubset