setOf_irrational

Mathlib.Topology.Instances.Irrational

URI: https://scilib.ai/kg/mathlib#IsGδ.setOf_irrational

English

The set of irrational numbers is a Gδ subset of the real line.

Русский

Множество иррациональных чисел является Gδ-подмножеством вещественной прямой.

LaTeX

$$$\operatorname{IsG\delta}(\{x \in \mathbb{R} \mid \operatorname{Irrational}(x)\})$$$

Lean4

protected theorem setOf_irrational : IsGδ {x | Irrational x} :=
  (countable_range _).isGδ_compl

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

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

Разделы

Аффилиация

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