lastFun_appendFun

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.lastFun_appendFun

English

Taking the last coordinate after appending yields g: lastFun (f ::: g) = g.

Русский

После добавления последний координат равен g: lastFun (f ::: g) = g.

LaTeX

$$$\mathrm{lastFun}(\mathrm{f} ::: \mathrm{g}) = \mathrm{g}$$$

Lean4

@[simp]
theorem lastFun_appendFun {α α' : TypeVec n} {β β' : Type*} (f : α ⟹ α') (g : β → β') : lastFun (f ::: g) = g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru