wrepr — Mathlib

English

The W-representation map wrepr is defined as the composition recF with wMk' and repr, giving a canonical representative for each W-element.

Русский

Отображение канонического представителя wrepr задаёт канонический представитель каждого элемента W.

LaTeX

$$$\mathrm{wrepr} = \mathrm{recF} \circ (q.P.wMk' \circ \mathrm{repr})$$$

Lean4

/-- maps every element of the W type to a canonical representative -/
def wrepr {α : TypeVec n} : q.P.W α → q.P.W α :=
  recF (q.P.wMk' ∘ repr)

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