proposition: Lemma TotallyBoundedIsLocated : forall (X : MetricSpace) (Y : X -> Prop), TotallyBoundedSubset X Y -> locatedMetric X -> LocatedSubset X Y.
proof: Proof. intros X Y totalBound loc d e x ltde. pose ((1#2)*(e-d)) as approxLen. pose (d+approxLen) as demid. assert (0 < approxLen) as approxLenPos. { unfold approxLen. rewrite <- (Qmult_0_r (1#2)). apply Qmult_lt_l. reflexivity. unfold Qminus. rewrite <- Qlt_minus_iff. exact ltde. } assert (demid < e). { unfold demid, approxLen. apply (Qplus_lt_l _ _ (-(1#2)*e)). ring_simplify. apply Qmult_lt_l. reflexivity. exact ltde. } specialize (totalBound (exist _ _ approxLenPos)) as [l H0]. unfold proj1_sig in e0. destruct (LocatedFinite X loc l demid e x H) as [far|close]. + left. intros y H2 abs. specialize (e0 y H2) as [t [H3 H4]]. specialize (far t H3). specialize (H0 t H3). contradict far. apply (ball_triangle X d approxLen _ _ _ abs) in H4. exact H4. + right. destruct close as [y [yin close]]. exists y. split. exact (H0 y yin). exact close. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Compact