length_map — Mathlib

English

The length of a walk is preserved under mapping by a graph homomorphism: the mapped walk has the same length as the original.

Русский

Длина обхода сохраняется под отображением графом-гомоморфизмом: образованный обход имеет ту же длину, что и исходный.

LaTeX

$$$(p.map\, f).length = p.length$$$

Lean4

@[simp]
theorem length_map : (p.map f).length = p.length := by induction p <;> simp [*]

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