finEncodingNatΓ'

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.finEncodingNatΓ'

English

A binary FinEncoding of ℕ into Γ' is given by finEncodingNatΓ'.

Русский

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

LaTeX

$$$ \text{finEncodingNatΓ'} : FinEncoding\,\mathbb{N} $$$

Lean4

/-- A binary FinEncoding of ℕ in Γ'. -/
def finEncodingNatΓ' : FinEncoding ℕ :=
  ⟨encodingNatΓ', inferInstanceAs (Fintype Γ')⟩

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

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

Разделы

Аффилиация

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