# Topology of irrational numbers #

In this file we prove the following theorems:

• IsGδ.setOf_irrational, dense_irrational, eventually_residual_irrational: irrational numbers form a dense Gδ set;

• Irrational.eventually_forall_le_dist_cast_div, Irrational.eventually_forall_le_dist_cast_div_of_denom_le; Irrational.eventually_forall_le_dist_cast_rat_of_denom_le: a sufficiently small neighborhood of an irrational number is disjoint with the set of rational numbers with bounded denominator.

We also provide OrderTopology, NoMinOrder, NoMaxOrder, and DenselyOrdered instances for {x // Irrational x}.

## Tags #

irrational, residual

@[deprecated IsGδ.setOf_irrational]
theorem isGδ_irrational :
IsGδ {x : | }

Alias of IsGδ.setOf_irrational.

theorem dense_irrational :
Dense {x : | }
theorem eventually_residual_irrational :
∀ᶠ (x : ) in ,
theorem Irrational.eventually_forall_le_dist_cast_div {x : } (hx : ) (n : ) :
∀ᶠ (ε : ) in nhds 0, ∀ (m : ), ε dist x (m / n)
theorem Irrational.eventually_forall_le_dist_cast_div_of_denom_le {x : } (hx : ) (n : ) :
∀ᶠ (ε : ) in nhds 0, kn, ∀ (m : ), ε dist x (m / k)
theorem Irrational.eventually_forall_le_dist_cast_rat_of_den_le {x : } (hx : ) (n : ) :
∀ᶠ (ε : ) in nhds 0, ∀ (r : ), r.den nε dist x r