English
For a function f: α → β, Sym.map f acts by applying f to every element of the underlying n-tuple.
Русский
Для функции f: α → β отображение Sym.map f действует путём применения f к каждому элементу n‑кортежа.
LaTeX
$$$\\forall f : \\alpha \\to \\beta,\\forall s : \\mathrm{Sym}(\\alpha,n),\\mathrm{Sym.map}(f)(s) = \\langle (s.\\mathrm{val}).\\mathrm{map} f, \\text{proof} \\rangle.$$$
Lean4
/-- A function `α → β` induces a function `Sym α n → Sym β n` by applying it to every element of
the underlying `n`-tuple. -/
def map {n : ℕ} (f : α → β) (x : Sym α n) : Sym β n :=
⟨x.val.map f, by simp⟩
