head_darts_fst — Mathlib

English

If the walk darts list is nonempty, the first dart's first coordinate equals the starting vertex.

Русский

Если список дротиков ненулевой, то первый дротик имеет первую координату, равную начальной вершине.

LaTeX

$$$ (p.darts.head\; hp).\mathrm{fst} = a $$$

Lean4

@[simp]
theorem head_darts_fst {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) : (p.darts.head hp).fst = a :=
  by
  cases p
  · contradiction
  · simp

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