English
For any path p, the property that getVert is injective on indices up to length(p) is equivalent to p being a path.
Русский
Для любого пути p свойство инъективности функции getVert на индексах до length(p) эквивалентно тому, что p является путём.
LaTeX
$$p.IsPath \iff Set.InjOn p.getVert (setOf (\lambda i. i \le p.length))$$
Lean4
theorem getVert_injOn_iff (p : G.Walk u v) : Set.InjOn p.getVert {i | i ≤ p.length} ↔ p.IsPath :=
by
refine ⟨?_, fun a => a.getVert_injOn⟩
induction p with
| nil => simp
| cons h q ih =>
intro hinj
rw [cons_isPath_iff]
refine
⟨ih (by
intro n hn m hm hnm
simp only [Set.mem_setOf_eq] at hn hm
have :=
hinj (by rw [length_cons]; cutsat : n + 1 ≤ (q.cons h).length)
(by rw [length_cons]; cutsat : m + 1 ≤ (q.cons h).length) (by simpa [getVert_cons] using hnm)
cutsat),
fun h' => ?_⟩
obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
have :=
hinj (by rw [length_cons]; cutsat : (n + 1) ≤ (q.cons h).length) (by cutsat : 0 ≤ (q.cons h).length)
(by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
omega
