dropLast_concat — Mathlib

English

If p is a walk and h is an adjacent edge, then dropping the last vertex after concatenation returns the original walk (up to equality): (p.concat h).dropLast = p.copy rfl.

Русский

Если дан ход p и смежное ребро h, то после конкатенации и удаления последней вершины получаем исходный ход: (p.concat h).dropLast = p.copy rfl.

LaTeX

$$$ (p.concat\\ h).dropLast = p.copy\\ rfl $$$

Lean4

@[simp]
theorem dropLast_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) : (p.concat h).dropLast = p.copy rfl (by simp) :=
  by
  induction p
  · rfl
  · simp_rw [concat_cons]
    rw [dropLast_cons_of_not_nil]
    · simp [*]
    · simp [concat, nil_iff_length_eq]

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