English
If n is strictly less than the number of vertices of p, then p can be split at the vertex p.vertices[n] into p1: a→v and p2: v→b with p = p1 ∘ p2 and p1.length = n.
Русский
Если n меньше количества вершин p, тогда p можно разложить в вершине p.vertices[n] как p1: a→v и p2: v→b при этом p = p1 ∘ p2 и p1.length = n.
LaTeX
$$$\exists v\exists p_1: Path\ a\ v\;\exists p_2: Path\ v\ b,\; p = p_1.comp p_2 ∧ p_1.length = n ∧ v = p.vertices[n]$$$
Lean4
/-- `split_at_vertex` decomposes a path `p` at the vertex sitting in
position `i` of its `vertices` -/
theorem exists_eq_comp_and_length_eq_of_lt_length (n : ℕ) (hn : n < p.vertices.length) :
∃ (v : V) (p₁ : Path a v) (p₂ : Path v b), p = p₁.comp p₂ ∧ p₁.length = n ∧ v = p.vertices[n] :=
by
have hn_le_len : n ≤ p.length := by
rw [vertices_length] at hn
exact Nat.le_of_lt_succ hn
obtain ⟨v, p₁, p₂, rfl, rfl⟩ := p.exists_eq_comp_of_le_length hn_le_len
exact ⟨v, p₁, p₂, rfl, rfl, by simp⟩
