fromAppend1DropLast

Mathlib.Data.TypeVec

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

← MathLib Explorer

English

The inverse arrow reconstructs α from the pair (drop α ::: last α).

Русский

Обратная стрелa восстанавливает α из пары (drop α ::: last α).

LaTeX

$$$\mathrm{fromAppend1DropLast} : (\mathrm{drop}\alpha ::: \mathrm{last}\alpha) \Rightarrow \alpha$$$

Lean4

/-- stitch two bits of a vector back together -/
def fromAppend1DropLast {α : TypeVec (n + 1)} : (drop α ::: last α) ⟹ α :=
  Arrow.mp (append1_drop_last _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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