proposition: Lemma CompactGraph_correct1 : forall plX plFEX x s, (inCompact x s) -> inCompact (Couple (x,(Cmap plX f x))) (CompactGraph plFEX s).
proof: Proof. intros plX plFEX x s Hs. unfold CompactGraph. setoid_replace (Couple (X:=X) (Y:=Y) (x, (Cmap plX f x))) with (Cmap plX graphPoint x). auto using CompactImage_correct1. intros e1 e2. rewrite Qplus_0_r. split;simpl. unfold graphPoint_modulus. eapply ball_weak_le;[|apply regFun_prf]. destruct (mu f e2); simpl. assert (Qmin (proj1_sig e2) (proj1_sig q) <= proj1_sig e2) by auto with *. rewrite -> Qle_minus_iff in *. rewrite Q_Qpos_min. rewrite <- Qle_minus_iff. apply Qplus_le_r. rewrite <- Qle_minus_iff in H. exact H. apply Qle_refl. apply (mu_sum plX e2 (e1::nil) f). simpl. unfold graphPoint_modulus. eapply ball_ex_weak_le;[|apply regFun_prf_ex]. destruct (mu f e1) as [d0|]; try constructor. destruct (mu f e2) as [d|]; try constructor. simpl. rewrite Q_Qpos_min. assert (Qmin (proj1_sig e2) (proj1_sig d) <= proj1_sig d) by auto with *. apply Qplus_le_r. exact H. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.metric2.Compact CoRN.metric2.Prelength CoRN.metric2.CompleteProduct CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax CoRN.logic.Classic