proposition: Lemma BishopCompactAsCompact_prf : forall P (HP:CompactSubset _ P), is_RegularFunction (@ball (FinEnum X)) (BishopCompactAsCompact_raw HP).
proof: Proof. cut (forall (P : RegularFunction (@ball X) -> Prop) (HP : CompactSubset (Complete X) P) (e1 e2 : Qpos), hemiMetric X (proj1_sig e1 + proj1_sig e2) (fun a : X => InFinEnumC a (let (l, _, _) := totallyBoundedSubset HP ((1 # 2) * e1)%Qpos in map (fun x : RegularFunction (@ball X) => approximate x ((1 # 2) * e1)%Qpos) l)) (fun a : X => InFinEnumC a (let (l, _, _) := totallyBoundedSubset HP ((1 # 2) * e2)%Qpos in map (fun x : RegularFunction (@ball X) => approximate x ((1 # 2) * e2)%Qpos) l))). intros Z P [HP0 HP HP1] e1 e2. split. apply (Qpos_nonneg (e1+e2)). split. apply Z. apply (hemiMetric_wd1 X (proj1_sig (e2+e1)%Qpos)). simpl; ring. apply Z. intros P [HP0 HP HP1] e1 e2 x Hx. unfold totallyBoundedSubset in Hx. destruct (HP ((1 # 2) * e1)%Qpos) as [l Hl0 Hl1]. unfold totallyBoundedSubset. destruct (HP ((1 # 2) * e2)%Qpos) as [r Hr0 Hr1]. simpl in *. assert (Z0:existsC (Complete X) (fun x' => In x' l /\ ball ((1#2)*proj1_sig e1) (Cunit x) x')). clear - Hx HP1. induction l. exfalso; exact (FinSubset_ball_nil Hx). simpl in Hx. apply FinSubset_ball_orC in Hx. destruct Hx as [ G | Hx | Hx] using orC_ind. auto using existsC_stable. apply existsWeaken. exists a. split; auto with *. rewrite -> Hx. apply (@ball_approx_l _ _ ((1#2)*e1)%Qpos). destruct (IHl Hx) as [G | z [Hz0 Hz1]] using existsC_ind. auto using existsC_stable. apply existsWeaken. exists z. auto with *. destruct Z0 as [ G | z [Hz0 Hz1] ] using existsC_ind. auto using existsC_stable. destruct (Hr1 _ (Hl0 _ Hz0)) as [ y [Hy0 Hy1]]. apply existsWeaken. exists (approximate y (Qpos2QposInf ((1#2)%Qpos*e2))). split. clear - Hy0. induction r. elim Hy0. destruct Hy0 as [Hy0 | Hy0]. rewrite Hy0. intro abs; contradict abs. exists (approximate y ((1 # 2) * e2)%Qpos). split. left. reflexivity. reflexivity. apply FinSubset_ball_cons. apply IHr; auto. setoid_replace (proj1_sig e1+proj1_sig e2) with (proj1_sig ((1#2)*e1 + (1#2)*e2 + (1#2)*e2 + (1#2)*e1))%Qpos by (simpl; ring). apply ball_weak. apply Qpos_nonneg. rewrite <- ball_Cunit. repeat eapply ball_triangle. apply Hz1. change (ball (proj1_sig ((1 # 2) * e2)%Qpos) z y) in Hy1. apply Hy1. apply ball_approx_r. 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