English
If p is a path from u to v and w lies on p with w ≠ v, then v does not belong to the vertex support of the initial segment p.takeUntil w.
Русский
Если p — путь от u до v, и вершина w принадлежит p, причем w ≠ v, то вершина v не входит в опору начального отрезка p.takeUntil w.
LaTeX
$$$ \forall {V} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v}, p.IsPath \to (w \in p.support) \to v \neq w \to v \notin (p.takeUntil w (hw)).support$$$
Lean4
/-- Taking a strict initial segment of a path removes the end vertex from the support. -/
theorem endpoint_notMem_support_takeUntil {p : G.Walk u v} (hp : p.IsPath) (hw : w ∈ p.support) (h : v ≠ w) :
v ∉ (p.takeUntil w hw).support := by
intro hv
rw [Walk.mem_support_iff_exists_getVert] at hv
obtain ⟨n, ⟨hn, hnl⟩⟩ := hv
rw [getVert_takeUntil hw hnl] at hn
have := p.length_takeUntil_lt hw h.symm
have : n = p.length := hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by simp) (hn.symm ▸ p.getVert_length.symm)
cutsat
