instCoeFunForallFinHAddNatLengthOfNat

English

There is a canonical coercion from RelSeries r to Fin(length+1) → α, i.e., RelSeries behaves like a finite sequence of α.

Русский

Существует каноническое отображение из RelSeries r в Fin(length+1) → α, т.е. RelSeries ведёт себя как конечная последовательность α.

LaTeX

$$$ \\text{RelSeries}\\; r \\hookrightarrow (\\mathrm{Fin}(\\text{length}+1) \\to \\alpha) $$$

Lean4

instance : CoeFun (RelSeries r) (fun x ↦ Fin (x.length + 1) → α) :=
  { coe := RelSeries.toFun }

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