of_append_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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