Commit 2023-05-23 07:30 4ecc5d58

View on Github →

feat: port Topology.Instances.Irrational (#4244)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Irrational.lean

added theorem Irrational.eventually_forall_le_dist_cast_div

added theorem Irrational.eventually_forall_le_dist_cast_div_of_denom_le

added theorem Irrational.eventually_forall_le_dist_cast_rat_of_den_le

added theorem dense_irrational

added theorem eventually_residual_irrational

added theorem isGδ_irrational