weight_comp — Mathlib

English

The weight of the concatenation p ∘ q equals the product of the weights: weight(w)(p.comp q) = weight(w)(p) · weight(w)(q).

Русский

Вес конкатенации путей p и q равен произведению весов путей: weight(w)(p.comp q) = weight(w)(p) · weight(w)(q).

LaTeX

$$$\mathrm{weight}(w)(p\comp q) = \mathrm{weight}(w)(p) \cdot \mathrm{weight}(w)(q)$$$

Lean4

@[to_additive (attr := simp) addWeight_comp]
theorem weight_comp (w : ∀ {i j : V}, (i ⟶ j) → R) {a b c : V} (p : Path a b) (q : Path b c) :
    weight w (p.comp q) = weight w p * weight w q := by
  induction q with
  | nil => simp
  | cons _ _ ih => simp [ih, mul_assoc]

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