ae_not_liouville — Mathlib

English

Almost every real x is not a Liouville number (without an exponent).

Русский

Почти каждое действительное число не является числом Лиувилля.

LaTeX

$$$$ \mathrm{volume}\Big(\mathbb{R} \setminus \{ x \in \mathbb{R} : Liouville(x) \} \Big) = \text{volume}(\mathbb{R}) $$$$

Lean4

theorem ae_not_liouville : ∀ᵐ x, ¬Liouville x :=
  ae_not_liouvilleWith.mono fun _ h₁ h₂ => h₁ 3 (by norm_num) (h₂.liouvilleWith 3)

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