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 setOfPred_liouville_eq_iInter_iUnion : {x : ℝ | Liouville x} = ⋂ (n : ℕ), ⋃ (a : ℤ), ⋃ (b : ℤ), ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

@[deprecated setOfPred_liouville_eq_iInter_iUnion (since := "2026-07-09")]

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

Alias of setOfPred_liouville_eq_iInter_iUnion.

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

@[deprecated IsGδ.setOfPred_liouville (since := "2026-07-09")]

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

Alias of IsGδ.setOfPred_liouville.

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

@[deprecated setOfPred_liouville_eq_irrational_inter_iInter_iUnion (since := "2026-07-09")]

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)

Alias of setOfPred_liouville_eq_irrational_inter_iInter_iUnion.

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.