Cycle rule.

diff --git a/mst.tex b/mst.tex
index 85c8b455f20f518abd729b83618b9a760f1ef9d5..8b8e74f56b1c33c68c9f99fc8a05e1d672b3d55b 100644 (file)
--- a/mst.tex
+++ b/mst.tex
@@ -302,6 +302,19 @@ are colored, so by the Blue lemma all blue edges are in~$T_{min}$ and by the Red
 lemma all other (red) edges are outside~$T_{min}$, so the blue edges are exactly~$T_{min}$.
 \qed
 
+\para
+The Red lemma actually works in both directions and it can be used to characterize
+all non-MST edges, which will turn out to be useful in the latter chapters.
+
+\corn{Cycle rule}\id{cyclerule}%
+An~edge~$e$ is not contained in the MST iff it is the heaviest on some cycle.
+
+\proof
+The implication from the right to the left is the Red lemma. In the other
+direction, when~$e$ is not contained in~$T_{min}$, it is $T_{min}$-heavy (by
+Theorem \ref{mstthm}), so it is the heaviest edge on the cycle $T_{min}[e]+e$.
+\qed
+
 %--------------------------------------------------------------------------------
 
 \section{Classical algorithms}