Theorems · Theorem · combinatorics

Quiver.Path.weight_nonneg

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

If all edge weights are non-negative, then the weight of any path is non-negative.

Defined in

Mathlib.Combinatorics.Quiver.Path.Weight

Cited by

1 results in Mathlib

Foundations

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

Assumes

QuiverSemiringLinearOrderIsStrictOrderedRing