Theorems · Theorem · combinatorics

Quiver.Path.weightOfEPs_nonneg

∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  {w : V → V → R}, (∀ (i j : V), 0 ≤ w i j) → ∀ {i j : V} (p : Quiver.Path i j), 0 ≤ Quiver.Path.weightOfEPs w p

If all edge weights (given by a function on vertices) are non-negative, so is the path weight.

Defined in

Mathlib.Combinatorics.Quiver.Path.Weight

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

QuiverSemiringLinearOrderIsStrictOrderedRing