English
The edge mapping from walks to lists of unordered vertex-pairs is injective: if two walks have the same edge sequence, they are equal.
Русский
Отображение ходов графа в списки неупорядоченных пар вершин инъективно: одинаковые последовательности рёбер означают равенство ходов.
LaTeX
$$$ \text{Walk.edges}: G.Walk\,u\,v \to \mathrm{List}(\mathrm{Sym}^2(V)) \; \text{ is injective. }$$$
Lean4
theorem edges_injective {u v : V} : Function.Injective (Walk.edges : G.Walk u v → List (Sym2 V))
| .nil, .nil, _ => rfl
| .nil, .cons _ _, h => by simp at h
| .cons _ _, .nil, h => by simp at h
| .cons' u v c h₁ w₁, .cons' _ v' _ h₂ w₂, h =>
by
have h₃ : u ≠ v' := by rintro rfl; exact G.loopless _ h₂
obtain ⟨rfl, h₃⟩ : v = v' ∧ w₁.edges = w₂.edges := by simpa [h₁, h₃] using h
obtain rfl := Walk.edges_injective h₃
rfl
