last — Mathlib

English

Extract a univariate functor from an n+1-ary functor by taking the last coordinate at each a.

Русский

Из n+1-арного функторa извлекаем унарный функтор, беря последнюю координату для каждого a.

LaTeX

$$$\\text{last} : PFunctor\\quad\\text{with } A := P.A,\\ B a := (P.B a).\\text{last}$$$

Lean4

/-- Split polynomial functor, get a univariate functor
from an `n+1`-ary functor -/
def last : PFunctor where
  A := P.A
  B a := (P.B a).last

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