mathlib documentation

topology.instances.irrational

Topology of irrational numbers #

In this file we prove the following theorems:

We also provide order_topology, no_min_order, no_max_order, and densely_ordered instances for {x // irrational x}.

Tags #

irrational, residual

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