Fix \(n \in \mathbb {N}\), let \(\mathit{es}\) be a list of weighted edges over \(n\) vertices, and let \(\mathit{uf} : \mathrm{Fin}\, n \to \mathbb {N}\) be an initial union–find state. The greedy loop, which scans \(\mathit{es}\) in order and merges the endpoints of each edge only when they currently carry different representatives, yields a final state that induces the same partition of the vertices as the unconditional fold, which merges the endpoints of every edge of \(\mathit{es}\) in order without regard to their current components. That is, for all \(i, j : \mathrm{Fin}\, n\), nodes \(i\) and \(j\) share a representative in the greedy-loop state if and only if they share a representative in the unconditional-fold state.

Fix \(n \in \mathbb {N}\), and let \(\mathit{es}\) be a list of weighted edges over \(n\) vertices, \(\mathit{uf}\) a union-find state on \(n\) nodes, and \(\mathit{acc}\) a list of weighted edges over \(n\) vertices. Then running the edge-selection sweep on \(\mathit{es}\) from state \(\mathit{uf}\) with initial accumulator \(\mathit{acc}\) yields the reversal of \(\mathit{acc}\) concatenated (on the left) with the result of running the same sweep on \(\mathit{es}\) from the same state \(\mathit{uf}\) but with the empty accumulator.

Let \(n \in \mathbb {N}\), let \(\mathit{uf} : \mathrm{Fin}\, n \to \mathbb {N}\) be a union-find state, and let \(\mathit{es}\) be a list of weighted edges over \(n\) vertices. Merging into \(\mathit{uf}\) only the edges retained by the edge-selection sweep (running the sweep from \(\mathit{uf}\) with an empty accumulator) yields a union-find state inducing the same equivalence relation on nodes as merging all of \(\mathit{es}\) into \(\mathit{uf}\): for all \(i, j : \mathrm{Fin}\, n\), the two nodes share a representative after the first process exactly when they share a representative after the second.

Fix a number of nodes \(n\), a union-find state \(\mathit{uf} : \mathrm{Fin}\, n \to \mathbb {N}\), a weighted edge \(e\) over \(n\) vertices with endpoints \(u\) and \(v\), and a list \(\mathit{rest}\) of further weighted edges over \(n\) vertices. Suppose the two endpoints of \(e\) already have the same representative in \(\mathit{uf}\), that is, \(\mathit{uf}(u) = \mathit{uf}(v)\). Then the edge-selection sweep applied to the list \(e :: \mathit{rest}\) starting from state \(\mathit{uf}\) with empty accumulator returns exactly the same edge list as the sweep applied to \(\mathit{rest}\) starting from the same state \(\mathit{uf}\) with empty accumulator.

Fix a natural number \(n\) and a union-find state \(\mathit{uf}\) over \(n\) nodes, and let \(e\) be a weighted edge over \(n\) vertices — with endpoints \(u_e, v_e\) and weight \(w_e\) — followed by a list \(\mathit{rest}\) of further weighted edges. Suppose the endpoints of \(e\) lie in different components, that is, \(\mathit{uf}(u_e) \ne \mathit{uf}(v_e)\). Then the total weight of the edge-selection sweep applied to the list \(e :: \mathit{rest}\) starting from \(\mathit{uf}\) and an empty accumulator equals \(w_e\) plus the total weight of the sweep applied to \(\mathit{rest}\) starting from an empty accumulator and the state obtained by merging the components of \(u_e\) and \(v_e\) in \(\mathit{uf}\).

Let \(\mathit{edges}\) be a list of weighted edges on \(n\) vertices, sorted in nondecreasing order of weight, and let \(\mathit{uf}\) be a union-find state whose induced partition is exactly the reachability relation of some base edge list \(\mathit{base}\): for all vertices \(a\) and \(b\), the representatives \(\mathit{uf}(a)\) and \(\mathit{uf}(b)\) are equal if and only if \(a\) and \(b\) are joined by a path through the edges of \(\mathit{base}\). Let \(S\) be any list of edges, each of which occurs in \(\mathit{edges}\), such that merging all of \(S\) into \(\mathit{uf}\) and merging all of \(\mathit{edges}\) into \(\mathit{uf}\) yield the same partition of the vertices. Then the greedy sweep — which starts from \(\mathit{uf}\), scans \(\mathit{edges}\) in order, and keeps each edge exactly when its two endpoints lie in currently distinct components — produces a set of edges whose total weight is at most the total weight of \(S\).