proposition: Lemma CompactIsLocated : forall (X : MetricSpace) (Y : Compact X), locatedMetric X -> LocatedSubset (Complete X) (fun z => inCompact z Y).
proof: Proof. intros X Y loc d e x ltde. assert (0 < e-d) as emdPos. { apply Qlt_minus_iff in ltde. exact ltde. } pose (d+(1#5)*(e-d)) as oneFifth. pose (d+(3#10)*(e-d)) as threeTenths. assert (oneFifth < threeTenths). { apply Qplus_lt_r, Qmult_lt_r. exact emdPos. reflexivity. } destruct (LocatedFinite (Complete X) (Complete_located loc) (map Cunit (approximate Y (Qpos2QposInf ((1#5)*(exist _ _ emdPos))))) oneFifth threeTenths x H) as [far|close]. + left. exact (CompactIsLocated_far X Y x d e emdPos loc far). + right. exact (CompactIsLocated_close X Y x d e emdPos loc close). Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact