weightOfEPs_nonneg — Mathlib

English

If all edge weights (given by a function on vertices) are nonnegative, then the path weight is nonnegative.

Русский

Если веса рёбер, заданные функцией на вершинах, неотрицательны, то вес пути неотрицателен.

LaTeX

$$$\\displaystyle \\forall w: V \\to V \\to \\mathbb{R},\\; \\left(\\forall i,j:\\; 0 \\le w(i,j)\\right) \\Rightarrow \\forall p: \\mathrm{Path}(i,j),\\; 0 \\le \\mathrm{weightOfEPs}(w,p).$$$

Lean4

/-- If all edge weights (given by a function on vertices) are non-negative,
so is the path weight. -/
theorem weightOfEPs_nonneg {w : V → V → R} (hw : ∀ i j : V, 0 ≤ w i j) {i j : V} (p : Path i j) : 0 ≤ weightOfEPs w p :=
  by
  apply weight_nonneg
  intro i j e
  exact hw _ _

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