dest — Mathlib

English

Destructor for Fix F: returns the original F-structure from a Fix element, i.e., the destructor is inverse to the constructor up to quotients.

Русский

Деструктор Fix: возвращает исходную структуру F из элемента Fix, т.е. деструктор обратно к конструктору в рамках кватирования.

LaTeX

$$$\mathrm{Fix.dest} : \mathrm{Fix} F \alpha \to F (\alpha \append1 (\mathrm{Fix} F \alpha))$$$

Lean4

/-- Destructor for `Fix F` -/
def dest : Fix F α → F (append1 α (Fix F α)) :=
  Fix.rec (MvFunctor.map (appendFun id Fix.mk))

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