arrow_tgt — Mathlib

English

The map of a path preserves subinterval structure: the interval on the mapped path equals the map of the interval on the original path.

Русский

Отображение пути сохраняет структуру подинтервалов: интервал на отображённом пути равен отображению интервала на исходном пути.

LaTeX

$$$(f.map\\sigma).\\mathrm{interval}(j,l,h) = f.\\mathrm{interval}(j,l,h).map(\\sigma)$$$

Lean4

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

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