cons — Mathlib

English

Define cons for maps Fin n →₀ M to Fin (n+1) →₀ M by prepending a value y at position 0 and shifting others accordingly.

Русский

Определим cons для отображений Fin n →₀ M в Fin (n+1) →₀ M, добавляя значение y на нулевую позицию и сдвигая остальные индексы.

LaTeX

$$$\\mathrm{cons}(y,s) : \\mathrm{Fin}(n+1) \\to_0 M$$$

Lean4

/-- `cons` for maps `Fin n →₀ M`. See `Fin.cons` for more details. -/
def cons (y : M) (s : Fin n →₀ M) : Fin (n + 1) →₀ M :=
  Finsupp.equivFunOnFinite.symm (Fin.cons y s : Fin (n + 1) → M)

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