dense_liouville
theorem dense_liouville : Dense {x | Liouville x}
The theorem `dense_liouville` states that the set of Liouville numbers is dense in the real numbers. This means that every real number is either a Liouville number or a limit of a sequence of Liouville numbers. Remember, a Liouville number is a real number `x` that satisfies the property: for every natural number `n`, there exist integers `a` and `b` with `b > 1` such that the absolute difference between `x` and the rational number `a/b` is less than `1/b^n` and `x` is not equal to `a/b`.
More concisely: The set of Liouville numbers is dense in the real numbers, meaning every real number is a Liouville number or a limit of a sequence of Liouville numbers.
|
eventually_residual_liouville
theorem eventually_residual_liouville : ∀ᶠ (x : ℝ) in residual ℝ, Liouville x
The theorem named `eventually_residual_liouville` states that the set of Liouville numbers is a residual set. In other words, the set of Liouville numbers, which are real numbers `x` such that for every natural number `n`, there exist integers `a` and `b` with `1 < b` such that `0 < |x - a/b| < 1/b^n`, includes a countable intersection of dense open sets in the real number topological space.
More concisely: The set of Liouville numbers is a residual set in the real numbers, meaning it is the intersection of countably many dense open sets.
|