proposition: Lemma FinCompact_uc : is_UniformlyContinuousFunction FinCompact_fun Qpos2QposInf.
proof: Proof. cut (forall e (d1 d2:Qpos) (a b : FinEnum (Complete X)), (hemiMetric (Complete X) e (fun a0 : Complete X => InFinEnumC a0 a) (fun a : Complete X => InFinEnumC a b)) -> (hemiMetric X (proj1_sig d1 + e + proj1_sig d2) (fun a0 : X => InFinEnumC a0 (approximate (FinCompact_fun a) d1)) (fun a0 : X => InFinEnumC a0 (approximate (FinCompact_fun b) d2)))). - intros L e a b [_ [Hab0 Hab1]] d1 d2. split. apply (Qpos_nonneg (d1+e+d2)). split; auto. eapply hemiMetric_wd1;[|apply L;apply Hab1]. unfold QposEq; simpl; ring. - intros e d1 d2 a b Hab c Hc. simpl in Hc. unfold FinCompact_raw in Hc. assert (existsC (Complete X) (fun d => InFinEnumC d a /\ msp_eq c (approximate d d1))). clear - Hc. induction a as [|a a0]. exfalso; exact (FinSubset_ball_nil Hc). simpl in Hc. apply FinSubset_ball_orC in Hc. destruct Hc as [ G | Hc | Hc] using orC_ind. auto using existsC_stable. apply existsWeaken. exists a. split; auto. intro abs; contradict abs. exists a. split. left. reflexivity. reflexivity. destruct (IHa0 Hc) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. apply FinSubset_ball_cons. exact Hy0. destruct H as [ G | d [Hd0 Hd1]] using existsC_ind. auto using existsC_stable. destruct (Hab d Hd0) as [ G | z [Hz0 Hz1]] using existsC_ind. auto using existsC_stable. clear - Hd1 Hz0 Hz1. induction b. exfalso; exact (FinSubset_ball_nil Hz0). apply FinSubset_ball_orC in Hz0. destruct Hz0 as [ G | Hz0 | Hz0] using orC_ind. auto using existsC_stable. apply existsWeaken. exists (approximate a d2). split. intro abs; contradict abs. exists (approximate a d2). split. left. reflexivity. reflexivity. rewrite -> Hz0 in Hz1. rewrite -> Hd1. apply Hz1. destruct (IHb Hz0) as [G | y [Hy0 Hy1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists y. split; auto. apply FinSubset_ball_cons. exact Hy0. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround CoRN.metric2.Prelength