wDest'_wMk

Mathlib.Data.PFunctor.Multivariate.W

URI: https://scilib.ai/kg/mathlib#MvPFunctor.wDest'_wMk

← MathLib Explorer

English

Applying the destructor to wMk'^(x) recovers the original x.

Русский

Применение деструктора к wMk' (x) восстанавливает исходный x.

LaTeX

$$$ wDest' (wMk'\ x) = x $$$

Lean4

theorem wDest'_wMk {α : TypeVec n} (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
    P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩ := by rw [wDest', wRec_eq]

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

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

Разделы

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

Аффилиация

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