getVert_eq_end_iff — Mathlib

English

For a path p from u to w and i ≤ length(p), the vertex p.getVert i equals w only when i = length(p).

Русский

Для пути p от u до w и i ≤ length(p) вершина p.getVert i равна w тогда и только тогда, когда i = длина(p).

LaTeX

$$p.IsPath \land i \le p.length \Rightarrow (p.getVert i = w \iff i = p.length)$$

Lean4

theorem getVert_eq_end_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
    p.getVert i = w ↔ i = p.length :=
  by
  have := hp.reverse.getVert_eq_start_iff (by cutsat : p.reverse.length - i ≤ p.reverse.length)
  simp only [length_reverse, getVert_reverse, show p.length - (p.length - i) = i by cutsat] at this
  rw [this]
  cutsat

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