English
There exists a zero-length walk from u to v if and only if u = v.
Русский
Существует путь нулевой длины от u к v тогда и только тогда, когда u = v.
LaTeX
$$$(\exists p: G.Walk u v, \operatorname{length}(p) = 0) \iff u = v$$$
Lean4
theorem concat_inj {u v v' w : V} {p : G.Walk u v} {h : G.Adj v w} {p' : G.Walk u v'} {h' : G.Adj v' w}
(he : p.concat h = p'.concat h') : ∃ hv : v = v', p.copy rfl hv = p' := by
induction p with
| nil =>
cases p'
· exact ⟨rfl, rfl⟩
· exfalso
simp only [concat_nil, concat_cons, cons.injEq] at he
obtain ⟨rfl, he⟩ := he
simp only [heq_iff_eq] at he
exact concat_ne_nil _ _ he.symm
| cons _ _ ih =>
rw [concat_cons] at he
cases p'
· exfalso
simp only [concat_nil, cons.injEq] at he
obtain ⟨rfl, he⟩ := he
rw [heq_iff_eq] at he
exact concat_ne_nil _ _ he
· rw [concat_cons, cons.injEq] at he
obtain ⟨rfl, he⟩ := he
rw [heq_iff_eq] at he
obtain ⟨rfl, rfl⟩ := ih he
exact ⟨rfl, rfl⟩
