mathlib3 documentation

number_theory.liouville.residual

Density of Liouville numbers #

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

In this file we prove that the set of Liouville numbers form a dense set. We also prove a similar statement about irrational numbers.

theorem set_of_liouville_eq_Inter_Union  :
{x : | liouville x} = (n : ), (a b : ) (hb : 1 < b), metric.ball (a / b) (1 / b ^ n) \ {a / b}
theorem set_of_liouville_eq_irrational_inter_Inter_Union  :
{x : | liouville x} = {x : | irrational x} (n : ), (a b : ) (hb : 1 < b), metric.ball (a / b) (1 / b ^ n)

The set of Liouville numbers is a residual set.

theorem dense_liouville  :
dense {x : | liouville x}

The set of Liouville numbers in dense.