support_transfer — Mathlib

English

Transferring a walk first to H and then to K is the same as transferring directly to K with the appropriate composed hp.

Русский

Перенос обхода сначала к графу H, затем к графу K равен переносу непосредственно к K с соответствующим композиционным hp.

LaTeX

$$((p.transfer H hp).transfer K hp') = p.transfer K (p.edges_transfer hp ∘ hp')$$

Lean4

@[simp]
theorem support_transfer (hp) : (p.transfer H hp).support = p.support := by induction p <;> simp [*]

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