finEncodingNatBool

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.finEncodingNatBool

English

A binary FinEncoding of ℕ is given by unary encoding and its finite Γ'.

Русский

Дано бинарное FinEncoding ℕ через бинарное кодирование и Γ'.

LaTeX

$$$ \text{finEncodingNatBool} : \mathrm{FinEncoding}\,\mathbb{N} $$$

Lean4

/-- A binary fin_encoding of ℕ in bool. -/
def finEncodingNatBool : FinEncoding ℕ :=
  ⟨encodingNatBool, Bool.fintype⟩

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

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

Разделы

Аффилиация

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