weight_cons — Mathlib

English

Weight of a path extended by an edge e equals weight of the original path times the weight of e: weight(p.cons e) = weight(p) · w(e).

Русский

Вес пути, дополненного ребром e, равен весу исходного пути, умноженному на вес ребра e.

LaTeX

$$$\mathrm{weight}(w)(p.\mathrm{cons}\ e) = \mathrm{weight}(w)(p) \cdot w(e)$$$

Lean4

@[to_additive (attr := simp) addWeight_cons]
theorem weight_cons (w : ∀ {i j : V}, (i ⟶ j) → R) {a b c : V} (p : Path a b) (e : b ⟶ c) :
    weight w (p.cons e) = weight w p * w e := by simp [weight]

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