map_comp_apply — Mathlib

English

Applying map to a vertex yields the corresponding vertex at the image index.

Русский

Применение отображения к вершине дает вершину с индексом образа.

LaTeX

$$$\operatorname{map}\; f \bigl(\operatorname{vertex}(x)\bigr) = \operatorname{vertex}(f(x))$$$

Lean4

theorem map_comp_apply (f : X → Y) (g : Y → Z) (x : stdSimplex S X) : map g (map f x) = map (g.comp f) x :=
  by
  ext
  simp [FunOnFinite.linearMap_comp]

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