proposition: Lemma FinEum_map_ball : forall (f:X -> X) (e:Qpos) (s:FinEnum), (forall x, ball (proj1_sig e) x (f x)) -> ball (proj1_sig e) s (map f s).
proof: Proof. intros f e s H. induction s. split. apply Qpos_nonneg. - split; intros a b abs; apply (FinSubset_ball_nil b). - destruct IHs as [IHs0 IHs1]. split. apply Qpos_nonneg. split; intros x y abs; unfold InFinEnumC, FinSubset_ball in y; contradict y ; intros [y [iny H0]]. destruct iny. + subst y. specialize (abs (f a)). contradict abs. split. apply InFinEnumC_weaken. left. reflexivity. rewrite H0. apply H. + destruct IHs1 as [IHs1 _]. pose proof (@FinSubset_ball_wd x y 0 0 s eq_refl H0) as [_ H2]. specialize (IHs1 x (H2 (InFinEnumC_weaken y s H1))). unfold existsC in IHs1. contradict IHs1. intros z [H3 H4]. specialize (abs z). contradict abs. split. 2: exact H4. simpl. apply FinSubset_ball_cons. exact H3. + destruct iny. subst y. specialize (abs a). contradict abs. split. apply InFinEnumC_weaken. left. reflexivity. rewrite H0. apply ball_sym, H. destruct IHs1 as [_ IHs1]. pose proof (@FinSubset_ball_wd x y 0 0 (map f s) eq_refl H0) as [_ H2]. specialize (IHs1 x (H2 (InFinEnumC_weaken y _ H1))). unfold existsC in IHs1. contradict IHs1. intros z [H3 H4]. specialize (abs z). contradict abs. split. 2: exact H4. simpl. apply FinSubset_ball_cons. exact H3. 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