proposition: Lemma InFinEnumC_map : forall (X Y:MetricSpace) (f:X --> Y) a l, InFinEnumC a l -> InFinEnumC (f a) (map f l).
proof: Proof. intros. intro abs. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [y [H H0]]. contradict abs. exists (f y). split. apply in_map. exact H. rewrite H0. reflexivity. 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