weightOfEPs_pos — Mathlib

English

If all edge weights, given by a function on vertices, are positive, then the path weight defined from these weights is positive.

Русский

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

LaTeX

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

Lean4

/-- If all edge weights (given by a function on vertices) are positive, so is the path weight. -/
theorem weightOfEPs_pos {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_pos
  intro i j e
  exact hw _ _

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