of_append_left — Mathlib

English

If the concatenation p.append q is a trail, then p is a trail.

Русский

Если объединение обходов p и q является трайлом, то первый обход p — трайл.

LaTeX

$$$ (p.\mathrm{append}(q)).IsTrail \Rightarrow p.IsTrail $$$

Lean4

theorem of_append_left {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) : p.IsTrail :=
  by
  rw [isTrail_def, edges_append, List.nodup_append] at h
  exact ⟨h.1⟩

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