weight — Mathlib

English

A path is assigned a weight by multiplying the weights of its edges; the empty path has weight 1, and extending a path by an edge e multiplies the weight by w(e).

Русский

Чтобы задать вес пути, перемножают веса его ребер; пустой путь имеет вес 1, а добавление ребра e умножает вес на w(e).

LaTeX

$$$\mathrm{weight}(w)(\mathrm{Path.Nil}) = 1\quad\text{and}\quad \mathrm{weight}(w)(p\;\text{cons } e) = \mathrm{weight}(w)(p) \cdot w(e)$$$

Lean4

/-- The weight of a path is the product of the weights of its edges. -/
def weight (w : ∀ {i j : V}, (i ⟶ j) → R) : ∀ {i j : V}, Path i j → R
  | _, _, Path.nil => 1
  | _, _, Path.cons p e => weight w p * w e

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