proposition: Lemma Cmap2_curry : forall (A B C: MetricSpace) (Apl : PrelengthSpace A) (Bpl : PrelengthSpace B) (f : ProductMS A B --> C) (a : Complete A) (b : Complete B), @msp_eq (Complete C) (Cmap2 Apl Bpl (uc_curry f) a b) (uc_compose (Cmap (ProductMS_prelength Apl Bpl) f) undistrib_Complete_uc (a,b)).
proof: Proof. intros. intros e1 e2. rewrite Qplus_0_r. assert ((1#2)*proj1_sig e1 + proj1_sig e2 <= proj1_sig e1 + proj1_sig e2). { apply Qplus_le_l. rewrite <- (Qmult_1_l (proj1_sig e1)) at 2. apply Qmult_le_r. apply Qpos_ispos. discriminate. } apply (ball_weak_le _ _ _ H). apply (mu_sum (ProductMS_prelength Apl Bpl) e2 (((1#2)*e1)%Qpos :: nil) f). simpl. clear H. destruct (mu f (exist (Qlt 0) (1#2) (@eq_refl comparison Lt) * e1)). 2: reflexivity. destruct (mu f e2). 2: reflexivity. split; apply regFun_prf. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.metric2.Classification CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.metric2.Complete CoRN.metric2.LocatedSubset Coq.Unicode.Utf8