proposition: Lemma InApproxCompact : forall {X : MetricSpace} (K : Compact X) (x : X) (d:Qpos) (e : Q), InFinEnumC x (approximate K d) -> locatedMetric X -> proj1_sig d < e -> { y:Complete X | inCompact y K /\ ball e (Cunit x) y }.
proof: Proof. intros X K x d e inx locX ltde. pose ((1#2)*(e-proj1_sig d)) as d2. pose (d2 / (proj1_sig d + e)) as k. assert (0 < proj1_sig d + e) as depos. { apply (Qlt_trans _ (proj1_sig d+0)). rewrite Qplus_0_r. apply Qpos_ispos. apply Qplus_lt_r. apply (Qlt_trans _ (proj1_sig d)). apply Qpos_ispos. exact ltde. } assert (0 < d2) as d2pos. { unfold d2. apply (Qle_lt_trans _ ((1#2)*0)). discriminate. apply Qmult_lt_l. reflexivity. unfold Qminus. rewrite <- Qlt_minus_iff. exact ltde. } assert (0 < k) as kpos. { unfold k. apply (Qpos_ispos (exist _ _ d2pos * Qpos_inv (exist _ _ depos))%Qpos). } assert (k <= 1#2) as khalf. { unfold k. apply Qle_shift_div_r. exact depos. unfold d2. apply Qmult_le_l. reflexivity. unfold Qminus. rewrite Qplus_comm. apply Qplus_le_l. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. } exists (CompactTotallyBounded_fun locX K (exist _ _ kpos) d (exist _ _ d2pos) khalf inx). split. apply CompactTotallyBoundedInCompact. pose proof (CompactTotallyBoundedNotFar locX K (exist _ _ kpos) d (exist _ _ d2pos) khalf inx) as H. apply (ball_weak_le) with (e:= (((1 + proj1_sig (exist (Qlt 0) k kpos)) * proj1_sig d + proj1_sig (exist (Qlt 0) d2 d2pos)) / (1 - proj1_sig (exist (Qlt 0) k kpos)))). 2: exact H. simpl. apply Qle_shift_div_r. unfold Qminus. rewrite <- Qlt_minus_iff. apply (Qle_lt_trans _ _ _ khalf). reflexivity. apply (Qplus_le_l _ _ (e*k - proj1_sig d)). ring_simplify. rewrite <- Qmult_plus_distr_r. unfold k, Qdiv. rewrite <- Qmult_assoc. rewrite <- (Qmult_comm (proj1_sig d + e)), Qmult_inv_r, Qmult_1_r. unfold d2. rewrite <- Qmult_plus_distr_l. setoid_replace ((1 # 2) + (1 # 2)) with 1%Q by reflexivity. rewrite Qmult_1_l. ring_simplify. apply Qle_refl. intro abs. rewrite abs in depos. exact (Qlt_irrefl 0 depos). 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