proposition: Lemma FinEnum_map_uc : forall z X Y (f:X --> Y), is_UniformlyContinuousFunction (map f:FinEnum X -> FinEnum Y) (FinEnum_map_modulus z (mu f)).
proof: Proof. intros z X Y f e. cut (forall (a b : FinEnum X) (d:Qpos), (QposInf_le d (mu f e)) -> ball (proj1_sig d) a b -> ball (m:=FinEnum Y) (proj1_sig e) (map f a) (map f b)). { intros Z a b. unfold FinEnum_map_modulus. case_eq (mu f e). intros d Hd H. apply Z with d; auto. rewrite Hd. simpl; auto with *. intros He H. apply Z with z; auto. rewrite He. constructor. } revert e. cut (forall (e d:Qpos), (QposInf_le d (mu f e)) -> forall (s1 s2 : FinEnum X), hemiMetric X (proj1_sig d) (fun a => InFinEnumC a s1) (fun a => InFinEnumC a s2) -> hemiMetric Y (proj1_sig e) (fun a => InFinEnumC a (map f s1:FinEnum Y)) (fun a => InFinEnumC a (map f s2))). { intros Z e s1 s2 d Hd [H0 H1]. split. apply Qpos_nonneg. split; apply (Z e d Hd); apply H1. } intros e d Hd s1 s2. intros H a Ha. induction s1. exfalso; exact (FinSubset_ball_nil Ha). apply FinSubset_ball_orC in Ha. destruct Ha as [G | Ha | Ha] using orC_ind. auto using existsC_stable. assert (Ha0:InFinEnumC a0 (a0::s1)). intro abs; contradict abs. exists a0. split. left. reflexivity. reflexivity. destruct (H a0 Ha0) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists (f y). split. apply InFinEnumC_map; assumption. rewrite Ha. apply (uc_prf f). apply ball_ex_weak_le with d; auto. apply IHs1; auto. intros b Hb. apply H. apply (@FinSubset_ball_cons _ b). exact Hb. 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