English
Let c be a cycle in G from v to v, and let w be a vertex that occurs on c. Then the initial segment of c up to w, namely takeUntil w h, is a path.
Русский
Пусть c — цикл в графе G, начинающийся и заканчивающийся в вершине v, и пусть w — вершина, встречающаяся на пути c. Тогда префикс пути до вершины w, имеющий вид takeUntil w h, является простым путём.
LaTeX
$$$ \forall {V} {G : SimpleGraph V} {v w : V} [DecidableEq V] {c : G.Walk v v}, c.IsCycle \to \forall h : w \in c.support, (c.takeUntil w h).IsPath$$$
Lean4
theorem isPath_takeUntil {c : G.Walk v v} (hc : c.IsCycle) (h : w ∈ c.support) : (c.takeUntil w h).IsPath :=
by
by_cases hvw : v = w
· subst hvw
simp
rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc
exact (c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))
