proposition: Lemma CompactIsLocated_close : forall (X : MetricSpace) (Y : Compact X) (x : Complete X) (d e : Q) (emdPos : 0 < e - d), locatedMetric X -> (exists y : Complete X, In y (map Cunit (approximate Y ((1 # 5) * exist (Qlt 0) (e - d) emdPos)%Qpos)) /\ ball (d+(3#10)*(e-d)) x y) -> exists y : Complete X, inCompact y Y /\ ball e x y.
proof: Proof. intros. destruct H as [y [yin close]]. pose proof (@CompactTotalBoundNotFar X X0 Y (exist _ _ emdPos)) as H0. apply (HausdorffBallHausdorffBallStrong (Complete_located X0)) in H0. unfold proj1_sig in H0. destruct H0 as [H0 _]. specialize (H0 y (InFinEnumC_weaken _ _ _ yin) ((1#10)*(exist _ _ emdPos))%Qpos) as [z [H0 H2]]. exists z. split. apply inCompact_stable. intro abs. unfold InFinEnumC, FinSubset_ball in H0. contradict H0; intros [t [H0 H1]]. contradict abs. rewrite H1. apply (CompactTotallyBoundedA _ _ _ _ H0). apply (ball_triangle _ _ _ _ _ _ close) in H2. setoid_replace e with ((d+(3#10)*(e-d)) + ((3 # 5) * (e - d) + (1#10) * (e - d)))%Q. exact H2. ring. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact