eventually_residual_irrational — Mathlib

English

The irrationals form a residual (comeager) subset of the real line.

Русский

Иррациональные образуют резидуальное (многое встречающееся) подмножество вещественной прямой.

LaTeX

$$$\operatorname{Comeager}\bigl(\{x \in \mathbb{R} \mid \operatorname{Irrational}(x)\}\bigr)$$$

Lean4

theorem eventually_residual_irrational : ∀ᶠ x in residual ℝ, Irrational x :=
  residual_of_dense_Gδ .setOf_irrational dense_irrational

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