Density of Liouville numbers

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.

theorem setOf_liouville_eq_iInter_iUnion : {x : ℝ | Liouville x} = ⋂ (n : ℕ), ⋃ (a : ℤ), ⋃ (b : ℤ), ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

theorem IsGδ.setOf_liouville : IsGδ {x : ℝ | Liouville x}

@[deprecated IsGδ.setOf_liouville (since := "2024-02-15")]

theorem isGδ_setOf_liouville : IsGδ {x : ℝ | Liouville x}

Alias of IsGδ.setOf_liouville.

theorem setOf_liouville_eq_irrational_inter_iInter_iUnion : {x : ℝ | Liouville x} = {x : ℝ | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ), ⋃ (b : ℤ), ⋃ (_ : 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.