English
If edge weights are nonnegative, then the weight of any path is nonnegative.
Русский
Если веса рёбер неотрицательны, то вес любого пути неотрицателен.
LaTeX
$$$\\displaystyle \\left(\\forall i,j,e:\\; 0 \\le w(e)\\right) \\Rightarrow \\forall i,j:\\forall p: \\mathrm{Path}(i,j),\\; 0 \\le \\mathrm{weight}(w,p).$$$
Lean4
/-- If all edge weights are non-negative, then the weight of any path is non-negative. -/
theorem weight_nonneg {w : ∀ {i j : V}, (i ⟶ j) → R} (hw : ∀ {i j : V} (e : i ⟶ j), 0 ≤ w e) {i j : V} (p : Path i j) :
0 ≤ weight w p := by
induction p with
| nil => simp
| cons p e ih =>
have he : 0 ≤ w e := hw e
simpa [weight_cons] using mul_nonneg ih he