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 Gδ set. We also prove a similar statement about irrational numbers.

source
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}
source
theorem is_Gδ_set_of_liouville  :
is_Gδ {x : ℝ | liouville x}
source
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)
source
theorem eventually_residual_liouville  :
∀ᶠ (x : ℝ) in residual ℝ, liouville x

The set of Liouville numbers is a residual set.

source
theorem dense_liouville  :
dense {x : ℝ | liouville x}

The set of Liouville numbers in dense.