arrow_src — Mathlib

English

In a path in a simplicial set X, the source of the i-th edge of a 1-simplex equals the i-th vertex of the path.

Русский

У источника i-го ребра в пути в симплициальном множестве X равен i-ая вершина пути.

LaTeX

$$$X.\mathrm{map}(\delta 1)^{\mathrm{op}}(\mathrm{f.arrow}\ i) = \mathrm{f.vertex}\ i^{\mathrm{castSucc}}$$$

Lean4

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

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