English
If a vertex v occurs in the vertex list of p, then p can be written as a concatenation p1 ∘ p2 with p1: a→v and p2: v→b.
Русский
Если вершина v встречается во множестве вершин p, то p можно разложить как p1 ∘ p2, где p1: a→v и p2: v→b.
LaTeX
$$$v ∈ p.vertices \Rightarrow \exists p_1 : Path\ a\ v, \exists p_2 : Path\ v\ b,\; p = p_1.comp p_2$$$
Lean4
/-- If a vertex `v` occurs in the list of vertices of a path `p : Path a b`, then `p` can be
decomposed as a concatenation of a subpath from `a` to `v` and a subpath from `v` to `b`. -/
theorem exists_eq_comp_of_mem_vertices {v : V} (hv : v ∈ p.vertices) :
∃ (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ :=
by
obtain ⟨n, hn, rfl⟩ : ∃ n, ∃ hn : n < p.vertices.length, v = p.vertices[n] := exists_mem_iff_getElem.mp ⟨v, hv, rfl⟩
obtain ⟨v, p₁, p₂, hp, hv, rfl⟩ := p.exists_eq_comp_and_length_eq_of_lt_length n hn
exact ⟨p₁, p₂, hp⟩
