arrow_src — Mathlib

English

Two paths are equal if and only if they have equal vertices and equal edges.

Русский

Два пути равны тогда и только тогда, когда равны их вершины и рёбра.

LaTeX

$$$\\forall f,g:\\,X.Path(m),\\ (f.vertex = g.vertex) \\wedge (f.arrow = g.arrow) \\Rightarrow f = g$$$

Lean4

/-- The source of a 1-simplex in a path is identified with the source vertex. -/
theorem arrow_src (f : Path X m) (i : Fin m) : X.map (tr (δ 1)).op (f.arrow i) = f.vertex i.castSucc :=
  Path₁.arrow_src f i

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