English
Let there be a quiver with a weight function w on its edges, taking values in a totally ordered ring R, such that every edge weight w(e) > 0. Then for every path p from i to j, the path weight weight(w, p) is positive.
Русский
Пусть задана кверьова структура с весами w на рёбрах, значения которых лежат в упорядоченной кольцевой группе R, и для каждого ребра e: i → j выполняется w(e) > 0. Тогда для любого пути p с началом i и концом j вес пути weight(w, p) положителен.
LaTeX
$$$\\displaystyle \\left(\\forall i,j,e:\\; i \\to j, \\; 0 < w(e)\\right) \\Rightarrow \\forall i,j\\; \\forall p: \\mathrm{Path}(i,j),\\; 0 < \\mathrm{weight}(w,p).$$$
Lean4
/-- If all edge weights are positive, then the weight of any path is positive. -/
theorem weight_pos {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_pos ih he
