isChain_dartAdj_cons_darts — Mathlib

English

If a walk starts at vertex u and the first edge connects u to v, then the list with u followed by the successors is a chain under DartAdj.

Русский

Если обход начинается с вершины u и первая грань соединяет u и v, то список u :: p.darts образует цепь по DartAdj.

LaTeX

$$$\forall d:\\ G.Dart,\\ v,w,\\ (h: d.snd = v)\\\,\\(p:\\ G.Walk v w),\\ List.IsChain G.DartAdj (d :: p.darts)$$$

Lean4

theorem isChain_dartAdj_cons_darts {d : G.Dart} {v w : V} (h : d.snd = v) (p : G.Walk v w) :
    List.IsChain G.DartAdj (d :: p.darts) := by
  induction p generalizing d with
  | nil => exact .singleton _
  | cons h' p ih => exact .cons_cons h (ih rfl)

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