Theorems · Definition · number theory

LiouvilleWith

ℝ → ℝ → Prop

We say that a real number x is a Liouville number with exponent p : ℝ if there exists a real number C such that for infinitely many denominators n there exists a numerator m such that x ≠ m / n and |x - m / n| < C / n ^ p. A number is a Liouville number in the sense of Liouville if it is LiouvilleWith any real exponent.

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Cited by

52 results in Mathlib

Foundations

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