English
Fix a vertex a. If every hom-set a ⟶ b is a singleton for all b, then the function toList sending a path a b to its vertex list is injective for that fixed a.
Русский
Зафиксируем вершину a. Пусть для всех b множество стрел из a в b имеет по крайней мере одно, и вообще является единичным. Тогда отображение toList: Path a b → List V инъективно по фиксированной a.
LaTeX
$$$\\forall a,b,\\ Injective (toList:\\ Path\\ a\\ b\\to\\ List\\ V).$$$
Lean4
theorem toList_injective (a : V) : ∀ b, Injective (toList : Path a b → List V)
| _, nil, nil, _ => rfl
| _, nil, @cons _ _ _ c _ p f, h => by cases h
| _, @cons _ _ _ c _ p f, nil, h => by cases h
| _, @cons _ _ _ c _ p f, @cons _ _ _ t _ C D, h =>
by
simp only [toList, List.cons.injEq] at h
obtain ⟨rfl, hAC⟩ := h
simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]
