adj_snd — Mathlib

English

For any non-nil walk p, the second vertex p.snd is adjacent to the starting vertex v.

Русский

Для любого непустого хода p вершина p.snd смежна с начальной вершиной v.

LaTeX

$$$ \forall p:\ G.Walk v w, \neg p.Nil \Rightarrow G.Adj v p.snd $$$

Lean4

@[simp]
theorem adj_snd {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj v p.snd := by
  simpa using adj_getVert_succ p (by simpa [not_nil_iff_lt_length] using hp : 0 < p.length)

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