mathlib documentation

number_theory.liouville.residual

Density of Liouville numbers #

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)
theorem eventually_residual_liouville  :
∀ᶠ (x : ) in residual , liouville x

The set of Liouville numbers is a residual set.

theorem dense_liouville  :
dense {x : | liouville x}

The set of Liouville numbers in dense.