# mathlibdocumentation

topology.instances.irrational

# Topology of irrational numbers #

In this file we prove the following theorems:

• is_Gδ_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 order_topology, no_bot_order, no_top_order, and densely_ordered instances for {x // irrational x}.

## Tags #

irrational, residual

theorem is_Gδ_irrational  :
is_Gδ {x : |
theorem dense_irrational  :
dense {x : |
theorem eventually_residual_irrational  :
∀ᶠ (x : ) in ,
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem irrational.eventually_forall_le_dist_cast_div {x : } (hx : irrational x) (n : ) :
∀ᶠ (ε : ) in 𝓝 0, ∀ (m : ), ε dist x (m / n)
theorem irrational.eventually_forall_le_dist_cast_div_of_denom_le {x : } (hx : irrational x) (n : ) :
∀ᶠ (ε : ) in 𝓝 0, ∀ (k : ), k n∀ (m : ), ε dist x (m / k)
theorem irrational.eventually_forall_le_dist_cast_rat_of_denom_le {x : } (hx : irrational x) (n : ) :
∀ᶠ (ε : ) in 𝓝 0, ∀ (r : ), r.denom nε dist x r