==Доказательство корректности==
{{Лемма
|id=lemma1
|statement=Рассмотрим связный неориентированный взвешенный граф <tex> G = (V, E) </tex> с инъективной весовой функцией <tex>w : E \to \mathbb{R}</tex> .
Тогда после первой итерации главного цикла алгоритма Борувки получившийся подграф можно достроить до ''MST''.
|proof=Предположим обратное: пусть любое ''MST'' графа <tex>G</tex> не содержит <tex>T</tex>. Рассмотрим какое-нибудь ''MST''. Тогда существует ребро <tex>x</tex> из <tex>T</tex> такое что <tex>x</tex> не принадлежит ''MST''. Добавив ребро <tex>x</tex> в ''MST'', получаем цикл в котором <tex>x</tex> не максимально, т.к оно было минимальным. Тогда, исходя из [[Критерий Тарьяна минимальности остовного дерева|критерия Тарьяна]], получаем противоречие.
}}
{{Теорема
|id=th1. |statement=Алгоритм Борувки строит '''MST''.'|proof=Очевидно, что алгоритм Борувки строит в результате работы алгоритма получается дерево.Будем доказывать что после каждой итерации главного цикла в алгоритме Борувки текущий подграф Пусть <tex>T</tex> можно достроить до {{---}} минимальное остовное дерево графа <tex> G </tex>, а <tex> T''MST''. Докажем это по индукции</tex> {{---}} дерево полученное после работы алгоритма.
'''База. ''' Покажем, что <tex>n T = 1T'</tex> (см. [[#lemma1|Лемму]]).
'''Переход. ''' Пусть лес Предположим обратное <tex>T</tex>, получившийся после <tex>n</tex> итераций алгоритма, можно достроить до ''MST''. Докажем, что после <tex>n+1</tex> итерации получившийся лес <tex>\neq T'</tex> можно достроить до ''MST''. Предположим обратное: Пусть ребро <tex>Te'</tex> нельзя достроить до ''MST''. Тогда существует {{---}} первое окрашенное ребро дерева <tex>F</tex> = ''MSTT'' графа <tex>G</tex>, содержащее <tex>T</tex> и не содержащее принадлежащее дереву <tex>T'</tex>. Тогда рассмотрим цикл, получающийся добавлением в Пусть <tex>FP </tex> какого-нибудь ребра <tex>x</tex> из <tex>T' {{---}} T</tex>. На этом цикле имеется ребропуть, большее по весу чем ребро соединяющий в дереве <tex>xT </tex>, иначе компонента для которой вершины ребра <tex>xe' </tex> является минимальным ребром ни с кем больше ни связана. Исходя из [[Критерий Тарьяна минимальности остовного дерева|критерия Тарьяна]], получаем противоречие.
Понятно, что в момент, когда ребро <tex> e'</tex> красили, какое-то ребро <tex> P </tex> (назовем его <tex> e </tex>) не было покрашено. По алгоритму <tex> w(e) > w(e''Получаем) </tex>. ''' Однако тогда <tex>T- e + e'</tex> можно достроить до ''MST''{{---}} остовное дерево меньшего веса. Получили противоречение. Следовательно предположение индукции верно<tex> T = T'</tex>.
}}
