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
@[deprecated IsGδ.setOf_irrational]
Alias of IsGδ.setOf_irrational
.