wMk' — Mathlib

English

Constructor for the W-type of P: wMk' takes an element x of P.Obj (α ::: P.W α) and returns a W-tree by applying wMk to its components after splitting.

Русский

Конструктор W-типа P: wMk' принимает элемент x из P.Obj (α ::: P.W α) и возвращает дерево W, применив wMk к компонентам после разбиения.

LaTeX

$$$ wMk'\ {\alpha} (x) = P.wMk (a) (splitFun f') (lastFun f) \text{ for } x = ⟨a, f⟩.$$$

Lean4

/-- Constructor for the W-type of `P` -/
def wMk' {α : TypeVec n} : P (α ::: P.W α) → P.W α
  | ⟨a, f⟩ => P.wMk a (dropFun f) (lastFun f)

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