mathlib documentation


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:

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  :
theorem dense_irrational  :
dense {x : | irrational x}
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]