support_tail_of_not_nil — Mathlib

English

If p is a nonempty walk, then p.tail.support = p.support.tail (and the assumption p ≠ Nil is included).

Русский

Если p — непустой ход, то p.tail.support = p.support.tail (с учётом p ≠ Nil).

LaTeX

$$$ p.tail.support = p.support.tail \\quad\\text{for } p \\neq Nil $$$

Lean4

theorem support_tail_of_not_nil (p : G.Walk u v) (hnp : ¬p.Nil) : p.tail.support = p.support.tail := by
  match p with
  | .nil => simp only [nil_nil, not_true_eq_false] at hnp
  | .cons h q => simp only [tail_cons, getVert_cons_succ, support_copy, support_cons, List.tail_cons]

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