Theorems · Theorem · number theory

setOfPred_liouvilleWith_subset_aux

{x | ∃ p > 2, LiouvilleWith p x} ⊆
  ⋃ m,
    (fun x => x + ↑m) ⁻¹'
      ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.Measure

Cited by

2 results in Mathlib

Foundations

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