map_eq_of_eq — Mathlib

English

If p and q have identical vertex sequences for all indices, then p = q.

Русский

Если последовательности вершин ходов p и q совпадают во всех позициях, то p = q.

LaTeX

$$$ (\\forall k, p.getVert k = q.getVert k) \\Rightarrow p = q $$$

Lean4

/-- Unlike categories, for graphs vertex equality is an important notion, so needing to be able to
work with equality of graph homomorphisms is a necessary evil. -/
theorem map_eq_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') : p.map f = (p.map f').copy (h ▸ rfl) (h ▸ rfl) :=
  by
  subst_vars
  rfl

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