encodable

Mathlib.Logic.Encodable.Basic

URI: https://scilib.ai/kg/mathlib#Int.encodable

English

The integers ℤ are encodable, via a bijection with the natural numbers

Русский

Целые числа ℤ кодируемы, через биекцию с натуральными числами

LaTeX

$$$ \operatorname{Encodable}(\mathbb{Z}) $$$

Lean4

instance _root_.Int.encodable : Encodable ℤ :=
  ofEquiv _ Equiv.intEquivNat

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

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

Разделы

Аффилиация

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