getVert_eq_start_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem getVert_eq_start_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) : p.getVert i = u ↔ i = 0 :=
  by
  refine ⟨?_, by simp_all⟩
  intro h
  by_cases hi : i = 0
  · exact hi
  · apply hp.getVert_injOn (by rw [Set.mem_setOf]; cutsat) (by rw [Set.mem_setOf]; cutsat)
    simp [h]

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