map_vertex — Mathlib

English

For any f, the image of a vertex under map f is the vertex at f applied to its index.

Русский

Для любого f образ вершины через map f — вершина по индексу, преобразованному f.

LaTeX

$$$\operatorname{stdSimplex.map}\; f\; (\operatorname{vertex}(x)) = \operatorname{vertex}(f(x))$$$

Lean4

@[simp]
theorem map_vertex [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) : map (S := S) f (vertex x) = vertex (f x) := by
  aesop

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