Real edge-weighted graphs, total tree weight and minimum spanning trees

A real edge-weighted graph is a pair $(G,w)$, where $G$ is a finite graph and $w:E(G)\to\mathbb R$. For a spanning tree $T$ of $G$, its total weight is

$w(T):=\sum_{e\in E(T)}w(e)$

(Spanning trees of a graph, The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form, The reals form a totally ordered field). A minimum spanning tree, or MST, is a spanning tree $T$ satisfying $w(T)\le w(S)$ for every spanning tree $S$ of $G$.

If $G$ is connected, an MST exists: connectedness supplies a spanning tree, and the set of spanning trees is finite, so the finite nonempty set of their real weights has a least element. This is the order-dual form of the finite-set maximum principle (A finite graph is connected if and only if it has a spanning tree, The set of spanning trees of a finite graph is finite, Every nonempty finite set of reals has a maximum and a minimum). If $G$ is disconnected, it has no spanning tree and hence no MST.