Liouville — Mathlib

English

A Liouville number is a real x such that for every n ∈ ℕ there exist a,b ∈ ℤ with 1 < b and x ≠ a/b and |x − a/b| < 1/b^n.

Русский

Число Лиувилля — это действительное число x, для каждого n ∈ ℕ существует пара a,b ∈ ℤ, b>1 и x ≠ a/b, причём |x−a/b| < 1/b^n.

LaTeX

$$$\\text{Liouville}(x) := \\forall n\\in\\mathbb N,\\; \\exists a,b\\in\\mathbb Z,\\; 1

Lean4

/-- A Liouville number is a real number `x` such that for every natural number `n`, there exist
`a, b ∈ ℤ` with `1 < b` such that `0 < |x - a/b| < 1/bⁿ`.
In the implementation, the condition `x ≠ a/b` replaces the traditional equivalent `0 < |x - a/b|`.
-/
def Liouville (x : ℝ) :=
  ∀ n : ℕ, ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧ |x - a / b| < 1 / (b : ℝ) ^ n

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