weight_nonneg — Mathlib

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

Похожие утверждения