Commit 2021-10-23 14:30 bb71667d

feat(topology/instances/irrational): new file (#9872)

• move is_Gδ_irrational etc to a new file topology.instances.irrational;
• prove that a small ball around an irrational number is disjoint with the set of rational numbers with bounded denominators;
• prove order_topology, no_top_order, no_bot_order, and densely_ordered instances for {x // irrational x}.