Theorems · Theorem · number theory

Liouville.frequently_exists_num

∀ {x : ℝ}, Liouville x → ∀ (n : ℕ), ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

If x is a Liouville number, then for any n, for infinitely many denominators b there exists a numerator a such that x ≠ a / b and |x - a / b| < 1 / b ^ n.

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Cited by

1 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound