61
правка
Изменения
Добавлена часть доказательства
|statement=После окончания работы алгоритма Дейкстры для всех вершин <tex>u \in V(G)</tex> будет выполняться равенство <tex>d[u] = \delta(s, u)</tex>
|proof=
Рассмотрим инвариант основного цикла: в начале каждой итерации для всех вершин <tex>v \in S</tex> выполняется <tex>d[v] = \delta(s, uv)</tex>
'''Инициализация'''. Изначально множество <tex>S</tex> пусто, инвариант выполняется.
'''Сохранение'''. Покажем, что при каждой итерации инвариант сохраняется для каждой вершины, добавленной в <tex>S</tex>, для этого воспользуемся методом «от противного». Предположим, что <tex>u</tex> первая добавленная в <tex>S</tex> вершина, для которой равенство <tex>d[u] = \delta(s, u)</tex> не выполняется. Рассмотрим ситуацию, сложившуюся в начале итерации, в которой <tex>u</tex> будет добавлена в <tex>S</tex>. Рассмотрев кратчайший путь из <tex>s</tex> в <tex>u</tex>, можно получить противоречие, заключающееся в том, что на рассматриваемый момент справедливо равенство <tex>d[u] = \delta(s, u)</tex>. Должно выполняться условие <tex>u \neq s</tex>, так как <tex>s</tex> является первой вершиной, добавленной в <tex>S</tex> и в момент её добавления равенство <tex>d[u] = \delta(s, u)</tex> выполняется. Из условия <tex>u \neq s</tex> следует, в частности, что <tex>S</tex> не пусто. Из вершины <tex>s</tex> в вершину <tex>u</tex> должен существовать какой-нибудь путь, так как иначе выполняется соотношение <tex>d[u] = \delta(s, u) = \infty</tex>, нарушающее предположение о том, что равенство <tex>d[u] = \delta(s, u)</tex> не выполняется. Из существования пути следует, что существует и кратчайший путь <tex>p</tex> из <tex>s</tex> в <tex>u</tex>. Перед добавлением <tex>u</tex> в <tex>S</tex> путь <tex>p</tex> соединяет вершину из множества <tex>S</tex> с вершиноу принадлежащей маножеству <tex>V \setminus S</tex>. Рассмотрим первую вершину <tex>y</tex> на пути <tex>p</tex> принадлежащую <tex>V \setminus S</tex>, и положим, что её предшествует вершина <tex>x \in S</tex>. Тогда, как видно из рис.1, путь <tex>p</tex> можно разложить на составляющие <tex>s \overset{p_1}{\leadsto} x \to y \overset{p_2}{\leadsto} u</tex>.
}}
