end_mem_vertices — Mathlib

English

If p is a path from a to b, then its endpoint b is contained in the list of its vertices.

Русский

Если p — путь от a до b, то вершина b принадлежит списку вершин p.

LaTeX

$$$b \in p.vertices$$$

Lean4

@[simp]
theorem end_mem_vertices {a b : V} (p : Path a b) : b ∈ p.vertices :=
  by
  have h₁ : p.vertices.getLast (vertices_ne_nil p) = b := vertices_getLast p (vertices_ne_nil p)
  have h₂ := getLast_mem (l := p.vertices) (vertices_ne_nil p)
  simpa [h₁] using h₂

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