mathlib3 documentation

topology.instances.irrational

Topology of irrational numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_min_order, no_max_order, and densely_ordered instances for {x // irrational x}.

Tags #

irrational, residual

theorem is_Gδ_irrational :

is_Gδ {x : ℝ | irrational x}

theorem dense_irrational :

dense {x : ℝ | irrational x}

theorem eventually_residual_irrational :

∀ᶠ (x : ℝ) in residual ℝ, irrational x

@[protected, instance]

def irrational.subtype.order_topology :

order_topology {x // irrational x}

@[protected, instance]

def irrational.subtype.no_max_order :

no_max_order {x // irrational x}

@[protected, instance]

def irrational.subtype.no_min_order :

no_min_order {x // irrational x}

@[protected, instance]

def irrational.subtype.densely_ordered :

densely_ordered {x // irrational x}

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