down_computable

Mathlib.Computability.Reduce

URI: https://scilib.ai/kg/mathlib#ULower.down_computable

English

The downward operation in ULower yields a computable encoding.

Русский

Операция снижения в ULower даёт вычислимое кодирование.

LaTeX

$$$ (ULower\\mathrm{equiv}\\alpha).\\mathrm{Computable} $$$

Lean4

@[simp]
theorem down_computable {α} [Primcodable α] : (ULower.equiv α).Computable :=
  ⟨Primrec.ulower_down.to_comp, Primrec.ulower_up.to_comp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru