Distinct weights imply a unique minimum spanning tree (source code)

= Distinct weights imply a unique minimum spanning tree

For a finite connected weighted graph with distinct <edge> weights, <Kruskal's algorithm> produces the unique <minimum spanning tree>. If another optimal tree existed, take an <edge> belonging only to the algorithm's tree and slightly increase its weight without changing the strict <edge> order. The algorithm then returns exactly the same tree, which must still be optimal, but the other tree's weight is unchanged and is now strictly smaller, a contradiction. Distinct weights are sufficient, not necessary: a triangle with weights $1,1,2$ has a unique optimum formed from the two weight-one <edges>.