adj_getVert_succ — Mathlib

English

In any walk w from u to v, for every index i with i < length(w), the i-th and (i+1)-th vertices are adjacent in G.

Русский

В любом пути w от u к v для каждого i < length(w) вершины номер i и i+1 соседние в графе G.

LaTeX

$$$$\forall {u,v} (w : G.Walk\ u\ v),\ \forall i \in \mathbb{N},\ i < w.length \Rightarrow G.Adj(w.getVert(i), w.getVert(i+1)).$$$$

Lean4

theorem adj_getVert_succ {u v} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) : G.Adj (w.getVert i) (w.getVert (i + 1)) :=
  by
  induction w generalizing i with
  | nil => cases hi
  | cons hxy _ ih =>
    cases i
    · simp [getVert, hxy]
    · exact ih (Nat.succ_lt_succ_iff.1 hi)

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