English
In an acyclic graph, there is at most one path between any two vertices.
Русский
В ацикличном графе между любой парой вершин существует по крайней мере один путь, и он единственный.
LaTeX
$$$G.IsAcyclic \Rightarrow ∀ v w: V, ∀ p q: G.Path v w, p = q$$$
Lean4
theorem path_unique {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p q : G.Path v w) : p = q :=
by
obtain ⟨p, hp⟩ := p
obtain ⟨q, hq⟩ := q
rw [Subtype.mk.injEq]
induction p with
| nil =>
cases (Walk.isPath_iff_eq_nil _).mp hq
rfl
| cons ph p ih =>
rw [isAcyclic_iff_forall_adj_isBridge] at h
specialize h ph
rw [isBridge_iff_adj_and_forall_walk_mem_edges] at h
replace h := h.2 (q.append p.reverse)
simp only [Walk.edges_append, Walk.edges_reverse, List.mem_append, List.mem_reverse] at h
rcases h with h | h
·
cases q with
| nil => simp at hp
| cons _ q =>
rw [Walk.cons_isPath_iff] at hp hq
simp only [Walk.edges_cons, List.mem_cons, Sym2.eq_iff, true_and] at h
rcases h with (⟨h, rfl⟩ | ⟨rfl, rfl⟩) | h
· cases ih hp.1 q hq.1
rfl
· simp at hq
· exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hq.2
· rw [Walk.cons_isPath_iff] at hp
exact absurd (Walk.fst_mem_support_of_mem_edges _ h) hp.2
