map_vertex — Mathlib

English

The i-th vertex of the image path f.map σ is the image under σ of the i-th vertex of f at the left end, i.e., (f.map σ).vertex i = σ.app(op 0) (f.vertex i).

Русский

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

LaTeX

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

Lean4

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

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