dense_liouville — Mathlib

English

The Liouville numbers form a dense set in the real line, as shown via IsGδ and residual arguments.

Русский

Числа Лиувилля образуют плотное множество на вещественной прямой, что следует из аргументов IsGδ и резидуальности.

LaTeX

$$$$ Dense\big(\{ x : Liouville(x) \} \big). $$$$

Lean4

/-- The set of Liouville numbers in dense. -/
theorem dense_liouville : Dense {x | Liouville x} :=
  dense_of_mem_residual eventually_residual_liouville

Похожие утверждения