wrepr_wMk — Mathlib

English

On a constructor node, wrepr maps to the wMk' canonical form of the representation of the absolute value.

Русский

На узле-конструкторе wrepr отображает в каноническую форму wMk' соответствующего представления абсолютного значения.

LaTeX

$$$\mathrm{wrepr}(q.P.wMk\ a\ f'\ f) = q.P.wMk'\bigl( \mathrm{repr}( \mathrm{abs}( \mathrm{appendFun}\ id \mathrm{wrepr} \langle a, q.P.appendContents f' f \rangle )) \bigr)$$$

Lean4

theorem wrepr_wMk {α : TypeVec n} (a : q.P.A) (f' : q.P.drop.B a ⟹ α) (f : q.P.last.B a → q.P.W α) :
    wrepr (q.P.wMk a f' f) = q.P.wMk' (repr (abs (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))) := by
  rw [wrepr, recF_eq', q.P.wDest'_wMk]; rfl

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