vertices_comp — Mathlib

English

If p: Path a b and q: Path b c, then the vertices of p.comp q equal p.vertices.dropLast ++ q.vertices.

Русский

Если пути p: a→b и q: b→c, то вершины p.comp q равны p.vertices.dropLast ++ q.vertices.

LaTeX

$$$ (p \\mathbin{.}\\, q).vertices = p.vertices.dropLast \\;\\cup\\; q.vertices $$$

Lean4

@[simp]
theorem vertices_comp {a b c : V} (p : Path a b) (q : Path b c) :
    (p.comp q).vertices = p.vertices.dropLast ++ q.vertices := by
  induction q with
  | nil => simp
  | cons q' e ih => simp [ih]

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