lastFun — Mathlib

English

Extract the last coordinate function from an arrow between TypeVecs: lastFun f : last α → last β, where f : α ⟹ β.

Русский

Извлекаем последнюю координату стрелы между TypeVecs: lastFun f : last α → last β, где f : α ⟹ β.

LaTeX

$$$\mathrm{lastFun} : (\alpha \Rightarrow \beta) \to (\mathrm{last}\alpha \to \mathrm{last}\beta)$$$

Lean4

/-- split off the last function of an arrow -/
def lastFun {α β : TypeVec (n + 1)} (f : α ⟹ β) : last α → last β :=
  f Fin2.fz

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