let W be Function; for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
let G be finite Graph; for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
let P be oriented Chain of G; for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
let v1, v2 be Element of G; ( P is_orientedpath_of v1,v2 & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W )
assume that
A1:
P is_orientedpath_of v1,v2
and
A2:
W is_weight>=0of G
; ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
AcyclicPaths (v1,v2) <> {}
by A1, Th41;
then consider r being FinSequence of the carrier' of G such that
A3:
r in AcyclicPaths (v1,v2)
and
A4:
for s being FinSequence of the carrier' of G st s in AcyclicPaths (v1,v2) holds
cost (r,W) <= cost (s,W)
by Th50;
consider t being oriented Simple Chain of G such that
A5:
r = t
and
A6:
t is_acyclicpath_of v1,v2
by A3;
take
t
; t is_shortestpath_of v1,v2,W
thus
t is_orientedpath_of v1,v2
by A6; GRAPH_5:def 17 for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds
cost (t,W) <= cost (q,W)
hereby verum
let s be
oriented Chain of
G;
( s is_orientedpath_of v1,v2 implies cost (t,W) <= cost (s,W) )assume A7:
s is_orientedpath_of v1,
v2
;
cost (t,W) <= cost (s,W)then consider x being
Element of the
carrier' of
G * such that A8:
x in AcyclicPaths s
by Th41, SUBSET_1:4;
AcyclicPaths s c= AcyclicPaths (
v1,
v2)
by A7, Th38;
then A9:
cost (
r,
W)
<= cost (
x,
W)
by A4, A8;
cost (
x,
W)
<= cost (
s,
W)
by A2, A8, Th54;
hence
cost (
t,
W)
<= cost (
s,
W)
by A5, A9, XXREAL_0:2;
verum
end;