proposition: Lemma FinEnum_ball_closed : forall e a b, (forall d, 0 < d -> FinEnum_ball (e+d) a b) -> FinEnum_ball e a b.
proof: Proof. unfold FinEnum_ball, hausdorffBall. intros e a b Hab. split. - apply Qnot_lt_le. intro abs. specialize (Hab (-e * (1#2))). destruct Hab. rewrite <- (Qmult_0_l (1#2)). apply Qmult_lt_r. reflexivity. apply (Qplus_lt_l _ _ e). ring_simplify. exact abs. ring_simplify in H. rewrite <- (Qmult_0_r (1#2)) in H. apply Qmult_le_l in H. exact (Qlt_not_le _ _ abs H). reflexivity. - split; apply hemiMetric_closed; firstorder. 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