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

theorem IsGδ.setOf_irrational : IsGδ {x : ℝ | Irrational x}

theorem dense_irrational : Dense {x : ℝ | Irrational x}

theorem eventually_residual_irrational : ∀ᶠ (x : ℝ) in residual ℝ, Irrational x

instance Irrational.instOrderTopologySubtypeReal : OrderTopology { x : ℝ // Irrational x }

instance Irrational.instNoMaxOrderSubtypeReal : NoMaxOrder { x : ℝ // Irrational x }

instance Irrational.instNoMinOrderSubtypeReal : NoMinOrder { x : ℝ // Irrational x }

instance Irrational.instDenselyOrderedSubtypeReal : DenselyOrdered { x : ℝ // Irrational x }

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, ∀ k ≤ n, ∀ (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