cons_tail_eq — Mathlib

English

For any walk p that is nonempty, constructing the walk by cons-ing its adj_snd and tail recovers p: cons (p.adj_snd hp) p.tail = p for hp : ¬ p.Nil.

Русский

Для любого непустого хода p восстановление хода через конc (p.adj_snd hp) p.tail даёт исходный ход: cons (p.adj_snd hp) p.tail = p.

LaTeX

$$$ cons\\ (p.adj\\_snd\\ hp)\\ p.tail = p $$$

Lean4

theorem cons_tail_eq (p : G.Walk u v) (hp : ¬p.Nil) : cons (p.adj_snd hp) p.tail = p := by
  cases p with
  | nil => simp at hp
  | cons h q => simp only [getVert_cons_succ, tail_cons, cons_copy, copy_rfl_rfl]

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