map_arrow — Mathlib

English

The i-th arrow of the mapped path equals the image under σ on the i-th edge: (f.map σ).arrow i = σ.app(op 1) (f.arrow i).

Русский

i-е ребро образованного пути равно образу i-го ребра под действием σ: (f.map σ).arrow i = σ.app(op 1) (f.arrow i).

LaTeX

$$$(f.map\sigma).arrow i = \sigma.app(\mathrm{op}\,\langle 1\rangle) (f.arrow i)$$$

Lean4

@[simp]
theorem map_arrow (f : Path X n) (σ : X ⟶ Y) (i : Fin n) : (f.map σ).arrow i = σ.app (op ⦋1⦌) (f.arrow i) :=
  rfl

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