394
правки
Изменения
→Доказательство корректности
|statement=Рассмотрим связный неориентированный взвешенный граф <tex> G = (V, E) </tex> с весовой функцией <tex>w : E \to \mathbb{R}, w(e1)!= w(e2)</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> можно достроить до MST.
Докажем это по индукции.
* База: <tex>n</tex> = 1([[#lemma1|Лемма]]).
* Переход: Пусть лес , <tex>T</tex> получившийся после <tex>n</tex> итераций алгоритма , можно достроить до MST. Докажем , что после <tex>n + 1</tex>+1-й итерации получившийся лес <tex>T'</tex> можно достроить до MST.Предположим обратное: <tex>T'</tex> нельзя достроить до MST. Тогда существует <tex>F</tex> = MST графа <tex>G</tex>, содержащее <tex>T</tex> и не содержащее <tex>T'</tex>. Тогда рассмотрим цикл , получающийся добавлением в <tex>F</tex> какого-нибудь ребра <tex>x</tex> из <tex>T'</tex> - <tex>T</tex>. На этом цикле имеется ребро , большее по весу чем ребро <tex>x</tex>, иначе компонента для которой <tex>x</tex> является минимальным ребром ни с кем больше ни связана.Исходя из [[Критерий Тарьяна минимальности остовного дерева|критерия Тарьяна]] , получаем противоречие.
Получаем <tex>T'</tex> можно достроить до MST. Следовательно предположение индукции верно.
