proposition: Lemma CompactGraph_graph : forall (plX : PrelengthSpace X) plFEX p q1 q2 s, inCompact (Couple (p,q1)) (CompactGraph plFEX s) -> inCompact (Couple (p,q2)) (CompactGraph plFEX s) -> msp_eq q1 q2.
proof: Proof. intros plX plFEX p q1 q2 s Hq1 Hq2. transitivity (Cmap plX f p). symmetry. rewrite <- (CoupleCorrect2 p q1). refine (CompactGraph_correct3 _ _). apply Hq1. rewrite <- (CoupleCorrect2 p q2). refine (CompactGraph_correct3 _ _). apply Hq2. 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