dest' — Mathlib

English

Destructor for M-types: build a new P‑structure from the last component using a split of M.dest.

Русский

Деструктор для M‑типа: построение новой структуры P из последнего компонента с использованием разбиения dest.

LaTeX

$$$\\text{dest'} : {α} \\to P (α.append1 (P.M α))$$$

Lean4

/-- Destructor for M-type of `P` -/
def dest' {α : TypeVec n} {x : P.last.M} {a : P.A} {f : P.last.B a → P.last.M} (h : PFunctor.M.dest x = ⟨a, f⟩)
    (f' : M.Path P x ⟹ α) : P (α.append1 (P.M α)) :=
  ⟨a, splitFun (M.pathDestLeft P h f') fun x => ⟨f x, M.pathDestRight P h f' x⟩⟩

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