arrow_tgt — Mathlib

English

Let X be a simplicial set and f a path of length n in X. For every i in {0,...,n−1}, the target vertex of the i-th edge of the path equals the (i+1)-th vertex of the path.

Русский

Пусть X — симплициальное множество и f — путь длины n в X. Для каждого i из {0,...,n−1} целевая вершина i-го ребра пути равна (i+1)-й вершине пути.

LaTeX

$$$X.map(\delta_0).op\\(f.arrow i) = f.vertex i\\.succ$$$

Lean4

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

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