English
If p is a path, then the function that lists the vertices along p is injective on the initial segment of length p.length+1.
Русский
Если p — путь, отображение вершин вдоль p инъективно на начальном отрезке длины p.length+1.
LaTeX
$$p.IsPath \Rightarrow Set.InjOn p.getVert {i | i \le p.length}$$
Lean4
theorem getVert_injOn {p : G.Walk u v} (hp : p.IsPath) : Set.InjOn p.getVert {i | i ≤ p.length} :=
by
intro n hn m hm hnm
induction p generalizing n m with
| nil => simp_all
| @cons v w u h p ihp =>
simp only [length_cons, Set.mem_setOf_eq] at hn hm hnm
by_cases hn0 : n = 0 <;> by_cases hm0 : m = 0
· cutsat
· simp only [hn0, getVert_zero, Walk.getVert_cons p h hm0] at hnm
have hvp : v ∉ p.support := by aesop
exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(m - 1), ⟨hnm.symm, by cutsat⟩⟩)).elim
· simp only [hm0, Walk.getVert_cons p h hn0] at hnm
have hvp : v ∉ p.support := by simp_all
exact (hvp (Walk.mem_support_iff_exists_getVert.mpr ⟨(n - 1), ⟨hnm, by cutsat⟩⟩)).elim
· simp only [Walk.getVert_cons _ _ hn0, Walk.getVert_cons _ _ hm0] at hnm
have := ihp hp.of_cons (by cutsat : (n - 1) ≤ p.length) (by cutsat : (m - 1) ≤ p.length) hnm
cutsat
