:: deftheorem Def3 defines .min_DPath_cost GLIB_004:def 3 :
for G being _finite real-weighted WGraph
for x, y being set
for b₄ being Real holds
( ( ex W being DWalk of G st W is_Walk_from x,y implies ( b₄ = G .min_DPath_cost (x,y) iff ex W being DPath of G st
( W is_mincost_DPath_from x,y & b₄ = W .cost() ) ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ( b₄ = G .min_DPath_cost (x,y) iff b₄ = 0 ) ) );