cons_support_tail — Mathlib

English

If p is a walk from u to v, then the prefix starting from the head vertex u together with the tail's support yields the full support: u :: p.tail.support = p.support.

Русский

Если p — ход от u к v, то вершина-голова u вместе с опорой хвостa даёт полную опору: u :: p.tail.support = p.support.

LaTeX

$$$ u :: p.tail.support = p.support $$$

Lean4

@[simp]
theorem cons_support_tail (p : G.Walk u v) (hp : ¬p.Nil) : u :: p.tail.support = p.support := by
  rw [← support_cons (p.adj_snd hp), cons_tail_eq _ hp]

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