map — Mathlib

English

There is a natural induced map sending a point of stdSimplex S X to a corresponding point in stdSimplex S Y via a map f: X → Y.

Русский

Существует естественная индуцированная карта, отправляющая точку stdSimplex S X в соответствующую точку stdSimplex S Y через отображение f: X → Y.

LaTeX

$$$\mathrm{map}\; f : \mathrm{stdSimplex}\; S\; X \to \mathrm{stdSimplex}\; S\; Y$$$

Lean4

/-- The map `stdSimplex S X → stdSimplex S Y` that is induced by a map `f : X → Y`. -/
noncomputable def map (f : X → Y) (s : stdSimplex S X) : stdSimplex S Y :=
  ⟨FunOnFinite.linearMap S S f s, image_linearMap f (by aesop)⟩

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