encode

Mathlib.Computability.Partrec

URI: https://scilib.ai/kg/mathlib#Computable.encode

English

The encoding map encode: α → Encodable is computable.

Русский

Кодирование encode: α → Encodable вычислимо.

LaTeX

$$$\operatorname{encode}: \alpha \to \mathrm{Encodable}$ is computable.$$

Lean4

protected theorem encode : Computable (@encode α _) :=
  Primrec.encode.to_comp

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

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

Разделы

Аффилиация

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