vertices_head? — Mathlib

English

The head of the list of vertices of a path p is the starting vertex a.

Русский

Голова списка вершин пути p равна начальной вершине a.

LaTeX

$$$ p.vertices.head? = \\text{Some}(a) $$$

Lean4

/-- The head of the vertices list is the start vertex -/
@[simp]
theorem vertices_head? {a b : V} (p : Path a b) : p.vertices.head? = some a := by
  induction p with
  | nil => simp only [vertices_nil, head?_cons]
  | cons p' e ih => simp [ih]

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