isChain_adj_cons_support — Mathlib

English

If u is adjacent to v, then for any walk p from v to w, the list u followed by p.support is a chain with respect to adjacency.

Русский

Если u смежен с v, то для обхода p от v к w список u :: p.support образует цепь по графу смежности.

LaTeX

$$$\forall p:\\ G.Walk v w,\\ List.IsChain G.Adj (u :: p.\\support)$$$

Lean4

theorem isChain_adj_cons_support {u v w : V} (h : G.Adj u v) : ∀ (p : G.Walk v w), List.IsChain G.Adj (u :: p.support)
  | nil => .cons_cons h (.singleton _)
  | cons h' p => .cons_cons h (isChain_adj_cons_support h' p)

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