weightOfEPs_comp — Mathlib

English

WeightOfEPs is multiplicative over path composition: weightOfEPs w (p.comp q) = weightOfEPs w p · weightOfEPs w q.

Русский

WeightOfEPs сохраняет произведение по композиции путей: weightOfEPs w (p.comp q) = weightOfEPs w p · weightOfEPs w q.

LaTeX

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

Lean4

@[to_additive addWeightOfEPs_comp]
theorem weightOfEPs_comp (w : V → V → R) {a b c : V} (p : Path a b) (q : Path b c) :
    weightOfEPs w (p.comp q) = weightOfEPs w p * weightOfEPs w q := by simp [weightOfEPs, weight_comp]

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