proposition: Lemma undistrib_Located : forall (X Y : MetricSpace) (A : Complete (ProductMS X Y) -> Prop), LocatedSubset _ A -> LocatedSubset (ProductMS (Complete X) (Complete Y)) (fun xy => exists p, msp_eq p (undistrib_Complete xy) /\ A p).
proof: Proof. intros X Y A loc d e p ltde. destruct (loc d e (undistrib_Complete p) ltde) as [far|close]. - left. intros y H abs. destruct H as [q [H H0]]. apply (far q H0). rewrite H. intros d1 d2; split; simpl; apply abs. - right. destruct close as [y [Ay close]]. exists (distrib_Complete y). split. exists y. split. symmetry. apply undistrib_after_distrib_Complete. exact Ay. rewrite <- distrib_after_undistrib_Complete. split; intros d1 d2; apply close. Defined.
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