proposition: Lemma CompactIsLocated_far : forall (X : MetricSpace) (Y : Compact X) (x : Complete X) (d e : Q) (emdPos : 0 < e - d), locatedMetric X -> (forall y : Complete X, In y (map Cunit (approximate Y ((1 # 5) * exist (Qlt 0) (e - d) emdPos)%Qpos)) -> ~ ball (d+(1#5)*(e-d)) x y) -> forall y : Complete X, inCompact y Y -> ~ ball d x y.
proof: Proof. intros. intro abs. pose proof (@InCompact_approxC X X0 _ _ ((1#5)*(exist _ _ emdPos)) H0) as H1. contradict H1; intro H1. destruct H1 as [z [H1 H3]]. specialize (H (Cunit z) (in_map _ _ _ H1)). contradict H. apply (ball_triangle _ _ _ _ _ _ abs) in H3. exact H3. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact