Documentation

Mathlib.Topology.Instances.Irrational

Topology of irrational numbers #

In this file we prove the following theorems:

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

Tags #

irrational, residual

@[deprecated IsGδ.setOf_irrational]

Alias of IsGδ.setOf_irrational.

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