ext_getVert — Mathlib

English

If p and q have identical vertex sequences for all indices, then p = q.

Русский

Если последовательности вершин ходов p и q совпадают во всех позициях, то p = q.

LaTeX

$$$ (\\forall k, p.getVert k = q.getVert k) \\Rightarrow p = q $$$

Lean4

theorem ext_getVert {u v} {p q : G.Walk u v} (h : ∀ k, p.getVert k = q.getVert k) : p = q :=
  by
  wlog hpq : p.length ≤ q.length generalizing p q
  · exact (this (fun k ↦ (h k).symm) (le_of_not_ge hpq)).symm
  have : q.length ≤ p.length := by
    by_contra!
    exact (q.adj_getVert_succ this).ne (by simp [← h, getVert_of_length_le])
  exact ext_getVert_le_length (hpq.antisymm this) fun k _ ↦ h k

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