proposition: Lemma FinEnum_is_MetricSpace : is_MetricSpace FinEnum_ball.
proof: Proof. split. - intros e epos x. apply hausdorffBall_refl, epos. - intros e x y. apply hausdorffBall_sym. - intros e d x y z. apply hausdorffBall_triangle. - intros e x y. unfold FinEnum_ball. apply FinEnum_ball_closed. - intros. apply H. - intros e x y. apply hausdorffBall_stable. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength