Topology of irrational numbers

In this file we prove the following theorems:

• isGδ_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δ_irrational : IsGδ {x : ℝ | Irrational x}

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

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

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

Equations

• Irrational.instOrderTopologySubtypeRealIrrationalInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpacePseudoMetricSpacePreorderInstPreorderReal = (_ : OrderTopology { x : ℝ // Irrational x })

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

Equations

• Irrational.instNoMaxOrderSubtypeRealIrrationalLtInstLTReal = (_ : NoMaxOrder { x : ℝ // Irrational x })

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

Equations

• Irrational.instNoMinOrderSubtypeRealIrrationalLtInstLTReal = (_ : NoMinOrder { x : ℝ // Irrational x })

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

Equations

• Irrational.instDenselyOrderedSubtypeRealIrrationalLtInstLTReal = (_ : 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