instDenumerable

Mathlib.Data.Rat.Denumerable

URI: https://scilib.ai/kg/mathlib#Rat.instDenumerable

English

The rational numbers are denumerable (countable).

Русский

Рациональные числа счетны (перечислимы).

LaTeX

$$$\exists f : \mathbb{N} \to \mathbb{Q} \text{ bijective}$$$

Lean4

/-- **Denumerability of the Rational Numbers** -/
instance instDenumerable : Denumerable ℚ :=
  ofEncodableOfInfinite ℚ

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

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

Разделы

Аффилиация

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