map — Mathlib

English

For a finite X, the value map f on s at y equals the sum over x ∈ univ with f x = y of s x.

Русский

Для конечного X значение map f s на y равно сумме по всем x ∈ univ, где f x = y, s x.

LaTeX

$$$\text{map } f s y = \sum_{x \in \mathrm{univ}, f x = y} s x$$$

Lean4

/-- The map `(X → M) → (Y → M)` induced by a map `X → Y` between finite types. -/
noncomputable def map [Finite X] [Finite Y] (f : X → Y) (s : X → M) : Y → M :=
  Finsupp.equivFunOnFinite (Finsupp.mapDomain f (Finsupp.equivFunOnFinite.symm s))

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