wDest'_wMk'

Mathlib.Data.PFunctor.Multivariate.W

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

← MathLib Explorer

English

Eta-like property for wMk': applying wDest' after wMk' returns the original value.

Русский

Эта-подобное свойство для wMk': применение wDest' после wMk' возвращает исходное значение.

LaTeX

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

Lean4

theorem wDest'_wMk' {α : TypeVec n} (x : P (α.append1 (P.W α))) : P.wDest' (P.wMk' x) = x := by obtain ⟨a, f⟩ := x;
  rw [wMk', wDest'_wMk, split_dropFun_lastFun]

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

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

Разделы

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

Аффилиация

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