getVert_of_length_le — Mathlib

English

Let w be a walk from u to v in G. If the length of w satisfies length(w) ≤ i for some i ∈ ℕ, then the i-th vertex along w is v; i.e., the walk has already reached its end by step i.

Русский

Пусть w — путь из u в v в графе G. Если длина пути length(w) ≤ i, то i-ый вершиной по пути является v; то есть путь достигнет конца к шагу i.

LaTeX

$$$$\forall {u,v} \; (w : G.Walk\ u\ v),\ \forall i \in \mathbb{N},\; (\text{length}(w) \le i) \Rightarrow w.getVert(i) = v.$$$$

Lean4

theorem getVert_of_length_le {u v} (w : G.Walk u v) {i : ℕ} (hi : w.length ≤ i) : w.getVert i = v := by
  induction w generalizing i with
  | nil => rfl
  | cons _ _ ih =>
    cases i
    · cases hi
    · exact ih (Nat.succ_le_succ_iff.1 hi)

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