proposition: Lemma CompactImage_correct1 : forall (x : Complete X) (s : Compact X), inCompact x s -> inCompact (Cmap plX f x) (CompactImage s).
proof: Proof. intros x s H e1 e2. apply FinSubset_ball_closed. intros d1 d1pos. assert (Qeq (proj1_sig e1 + proj1_sig e2 + d1) (proj1_sig ((e1 + (1#4)*exist _ _ d1pos) + ((1#4)*exist _ _ d1pos + ((1#4)*exist _ _ d1pos)) + ((1#4)*exist _ _ d1pos + e2))%Qpos)) by (simpl; ring). apply (@FinSubset_ball_wd_full _ _ _ H0 _ _ (reflexivity _) _ _ (reflexivity _)). clear H0. apply FinSubset_ball_triangle_r with (approximate (CompactImage s) ((1#4)*exist _ _ d1pos)%Qpos); [|apply regFun_prf]. apply FinSubset_ball_triangle_l with (approximate (Cmap plX f x) ((1#4)*exist _ _ d1pos)%Qpos); [apply regFun_prf|]. remember (mu f ((1 # 4) * exist _ _ d1pos)) as dum. simpl. unfold FinEnum_map_modulus. simpl in Heqdum. rewrite <- Heqdum. destruct dum. - apply (FinSubset_ball_map2 ((1 # 4) * exist _ _ d1pos) ((1 # 4) * exist _ _ d1pos) (q+q)%Qpos). 2: apply H. simpl. simpl in Heqdum. rewrite <- Heqdum. apply Qle_refl. - assert (Z:=H z z). simpl in Z. destruct (@approximate _ (FinEnum_ball X) s z). exfalso; exact (FinSubset_ball_nil Z). intro abs; contradict abs. exists (f m). split. left. reflexivity. set (d:=((1 # 4) * exist _ _ d1pos)%Qpos). apply (mu_sum plX d (d::nil) f). simpl. unfold d. simpl. rewrite <- Heqdum. constructor. 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