support_append_eq_support_dropLast_append

English

If the concatenation p.append p' equals q.append q', then their tails satisfy a corresponding equality.

Русский

Если конкатенации p.append p' и q.append q' равны, то хвосты удовлетворяют соответствующему равенству.

LaTeX

$$$(p.\append p') = (q.\append q') \Rightarrow \exists ? hv, \text{tail equality of tails}$$$

Lean4

theorem support_append_eq_support_dropLast_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support = p.support.dropLast ++ p'.support := by
  induction p <;> simp_all [List.dropLast_cons_of_ne_nil]

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