isPath_of_append_right — Mathlib

English

If p is a nonempty path and p appended with q is a cycle, then q is a path.

Русский

Если p — непустой путь и p заканчивался циклом после добавления q, то q — путь.

LaTeX

$$¬p.Nil \land (p.append q).IsCycle \Rightarrow q.IsPath$$

Lean4

theorem isPath_of_append_right {p : G.Walk u v} {q : G.Walk v u} (h : ¬p.Nil) (hcyc : (p.append q).IsCycle) :
    q.IsPath := by
  have := hcyc.2
  rw [tail_support_append, List.nodup_append'] at this
  rw [isPath_def, support_eq_cons, List.nodup_cons]
  exact ⟨this.2.2 (p.end_mem_tail_support h), this.2.1⟩

Похожие утверждения