proposition: Lemma CompactImage_correct2 : forall (y : Complete Y) (s : Compact X), locatedMetric Y -> inCompact y (CompactImage s) -> forall d:Qpos, { x:X | ball (proj1_sig d) (approximate y ((1 # 3) * d)%Qpos) (f x) /\ In x (approximate s (FinEnum_map_modulus z (mu f) ((1 # 3) * d))) }.
proof: Proof. intros y s locY inys d. specialize (inys ((1#3)*d)%Qpos ((1#3)*d)%Qpos). simpl in inys. assert ((1#3)*proj1_sig d+(1#3)*proj1_sig d < proj1_sig d) as H. { rewrite <- Qmult_plus_distr_l. rewrite <- (Qmult_1_l (proj1_sig d)) at 2. apply Qmult_lt_r. apply Qpos_ispos. reflexivity. } destruct (AlmostInExists locY H inys) as [n H0]. destruct ( @nth_error (msp_car Y) (@map (msp_car X) (msp_car Y) (@ucFun X Y f) (@approximate (list (msp_car X)) (FinEnum_ball X) s (Qpos2QposInf (FinEnum_map_modulus z (@mu X Y f) (Qpos_mult (@exist Q (Qlt {| Qnum := Z0; Qden := xH |}) {| Qnum := Zpos xH; Qden := xI xH |} (@eq_refl comparison Lt)) d))))) n) as [t|] eqn:des. 2: contradiction. destruct (nth_error (approximate s (FinEnum_map_modulus z (mu f) ((1#3)*d))) n) eqn:H1. - exists m. split. 2: exact (nth_error_In _ _ H1). pose proof (map_nth_error f n _ H1). simpl in des. simpl in H2. rewrite des in H2. inversion H2. subst t. clear H2 des. exact H0. - exfalso. apply nth_error_None in H1. rewrite <- (map_length f) in H1. apply nth_error_None in H1. simpl in des. simpl in H1. rewrite des in H1. discriminate. 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